---

Step * of Lemma subtype_rel-equal

∀[A,B:Type].  A ⊆r B supposing A = B ∈ Type
BY
{ (Intros THEN SubtypeFromEq ) }

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  SubtypeFromEq  )

---

Home Index