---

Step * of Lemma ext-eq_transitivity

∀[A,B,C:Type].  (A ≡ C) supposing (B ≡ C and A ≡ B)
BY
{ (Unfold `ext-eq` 0 THEN Auto THEN ((D 0 THEN Auto) THEN SubsumeC ⌜B⌝⋅ THEN Auto THEN TrySubsume)⋅) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    (A  \mequiv{}  C)  supposing  (B  \mequiv{}  C  and  A  \mequiv{}  B)


By

---

Latex:
(Unfold  `ext-eq`  0  THEN  Auto  THEN  ((D  0  THEN  Auto)  THEN  SubsumeC  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  TrySubsume)\mcdot{})

---

Home Index