---

Step * of Lemma MTree_Node_wf

∀[T:Type]. ∀[labels:{L:Atom List| 0 < ||L||} ]. ∀[children:{a:Atom| (a ∈ labels)}  ─→ MultiTree(T)].
  (MTree_Node(labels;children) ∈ MultiTree(T))
BY
{ DepprodCoDatatypeConstructorWf `MultiTree_size` }

---

Latex:


\mforall{}[T:Type].  \mforall{}[labels:\{L:Atom  List|  0  <  ||L||\}  ].  \mforall{}[children:\{a:Atom|  (a  \mmember{}  labels)\}    {}\mrightarrow{}  MultiTree(T)].
    (MTree\_Node(labels;children)  \mmember{}  MultiTree(T))


By

DepprodCoDatatypeConstructorWf  `MultiTree\_size`

---

Home Index