(def-constant quotient 
    "lambda(rel:[ind_1,ind_1 -> prop], lambda(x:ind_1, indic{z:ind_1, rel(x,z)}))"
    (theory generic-theory-1))

(def-theorem quotient-map-for-equivalence-relations 
    "forall(rel:[ind_1,ind_1 -> prop], 
                      equiv%predicate(rel) 
                        implies
                      forall(x,y:ind_1, rel(x,y) iff quotient(rel)(x)=quotient(rel)(y)))"
    (usages transportable-macete)
    reverse
    (theory generic-theory-1)
    (proof
      (
        (apply-macete-with-minor-premises characterization-of-equivalence-predicates)
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)")
            extensionality
            simplify
            direct-and-antecedent-inference-strategy
            (block 
	(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
	simplify
	(backchain "with(p:prop,forall(a,b:ind_1,p));")
	(backchain "with(p:prop,forall(a,b,c:ind_1,p));")
	(instantiate-existential ("x"))
	(backchain "with(p:prop,forall(a,b:ind_1,p));"))
            (block 
	(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
	(contrapose "with(p:prop,not(p));")
	(backchain "with(p:prop,forall(a,b:ind_1,p));")
	(backchain "with(p:prop,forall(a,b,c:ind_1,p));")
	(instantiate-existential ("y"))
	(backchain "with(p:prop,forall(a,b:ind_1,p));")
	(backchain "with(p:prop,forall(a,b:ind_1,p));")))
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 1 0)")
            (contrapose "with(f:sets[ind_1],f=f);")
            extensionality
            simplify
            (instantiate-existential ("y"))
            simplify)
        )))