---

Step * of Lemma general-subtype-respects-equality

∀[A,B,C:Type].  (respects-equality(B;C)) supposing (respects-equality(A;C) and (B ⊆r A))
BY
{ (Intros THEN (Unhide THENA Auto) THEN RepeatFor 4 (ParallelLast) THEN SubsumeC ⌜B⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    (respects-equality(B;C))  supposing  (respects-equality(A;C)  and  (B  \msubseteq{}r  A))


By

---

Latex:
(Intros  THEN  (Unhide  THENA  Auto)  THEN  RepeatFor  4  (ParallelLast)  THEN  SubsumeC  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index