---

Step * of Lemma subtype_rel-labeled-graph

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

---

Latex:

---

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


By

---

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

---

Home Index