---

Step * of Lemma monotone-labeled-graph

∀[F:Type ─→ Type]. Monotone(T.LabeledGraph(F[T])) supposing Monotone(T.F[T])
BY
{ (Auto THEN Unfold `labeled-graph` 0 THEN SubtypeReasoning THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  Monotone(T.LabeledGraph(F[T]))  supposing  Monotone(T.F[T])


By

---

Latex:
(Auto  THEN  Unfold  `labeled-graph`  0  THEN  SubtypeReasoning  THEN  Auto)

---

Home Index