---

Step * of Lemma set-equal-equiv

∀[T:Type]. EquivRel(T List;x,y.set-equal(T;x;y))
BY
{ (RepUR ``set-equal equiv_rel trans sym refl`` 0 THEN Auto THEN (BackThruSomeHyp THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  EquivRel(T  List;x,y.set-equal(T;x;y))


By

---

Latex:
(RepUR  ``set-equal  equiv\_rel  trans  sym  refl``  0  THEN  Auto  THEN  (BackThruSomeHyp  THEN  Auto')\mcdot{})

---

Home Index