---

Step * of Lemma subtype-base-respects-equality

∀[A,B:Type].  respects-equality(B;A) supposing B ⊆r Base
BY
{ (Intros THEN InstLemma `general-subtype-respects-equality` [⌜Base⌝;⌜B⌝;⌜A⌝]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  InstLemma  `general-subtype-respects-equality`  [\mkleeneopen{}Base\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index