---

Step * of Lemma least-equiv-is-equiv

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  EquivRel(A;x,y.least-equiv(A;R) x y)
BY
{ (Intros THEN BLemma `least-equiv-is-equiv-1` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    EquivRel(A;x,y.least-equiv(A;R)  x  y)


By

---

Latex:
(Intros  THEN  BLemma  `least-equiv-is-equiv-1`  THEN  Auto)

---

Home Index