---

Step * of Lemma monotone-ldag

∀[F:Type ─→ Type]. Monotone(T.LabeledDAG(F[T])) supposing Monotone(T.F[T])
BY
{ (Auto THEN Unfold `ldag` 0 THEN D 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `ldag`  0  THEN  D  0  THEN  Auto)

---

Home Index