---

Step * of Lemma MMTree_Node_wf

∀[T:Type]. ∀[forest:MMTree(T) List List].  (MMTree_Node(forest) ∈ MMTree(T))
BY
{ DepprodCoDatatypeConstructorWf `MMTree_size` }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[forest:MMTree(T)  List  List].    (MMTree\_Node(forest)  \mmember{}  MMTree(T))


By

---

Latex:
DepprodCoDatatypeConstructorWf  `MMTree\_size`

---

Home Index