---

Step * of Lemma bar-equal-equiv

∀[T:Type]. EquivRel(bar-base(T);x,y.bar-equal(T;x;y))
BY
{ (Auto THEN Unfold `bar-equal` 0 THEN RepeatFor 2 ((D 0 THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `bar-equal`  0  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index