---

Step * of Lemma subtype_rel-ldag

∀[A,B:Type].  LabeledDAG(A) ⊆r LabeledDAG(B) supposing A ⊆r B
BY
{ (InstLemma `monotone-ldag` [⌜λ2T.T⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `monotone-ldag`  [\mkleeneopen{}\mlambda{}\msubtwo{}T.T\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index