---

Step * of Lemma equal_symmetry

∀[T:Type]. ∀[x,y:T].  uiff(x = y ∈ T;y = x ∈ T)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].    uiff(x  =  y;y  =  x)


By

---

Latex:
Auto

---

Home Index