---

Step * of Lemma Com-subtype

∀[M:Type ⟶ Type]
  ∀[A,B:Type].  (Com(P.M[P]) A) ⊆r (Com(P.M[P]) B) supposing A ⊆r B supposing ∀A,B:Type.  ((A ⊆r B) ⇒ (M[A] ⊆r M[B]))
BY
{ (RepUR ``Com`` 0 THEN Auto THEN RepeatFor 3 ((BLemma `subtype_rel_tagged+` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[A,B:Type].    (Com(P.M[P])  A)  \msubseteq{}r  (Com(P.M[P])  B)  supposing  A  \msubseteq{}r  B 
    supposing  \mforall{}A,B:Type.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (M[A]  \msubseteq{}r  M[B]))


By

---

Latex:
(RepUR  ``Com``  0  THEN  Auto  THEN  RepeatFor  3  ((BLemma  `subtype\_rel\_tagged+`  THEN  Auto)))

---

Home Index