---

Step * of Lemma ext-eq_weakening

∀[A,B:Type].  A ≡ B supposing A = B ∈ Type
BY
{ (Auto⋅ THEN RepeatFor 2 ((D 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    A  \mequiv{}  B  supposing  A  =  B


By

---

Latex:
(Auto\mcdot{}  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index