```
(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)
)))
```