---

Step * of Lemma MTree_Node-labels_wf

∀[T:Type]. ∀[v:MultiTree(T)].  MTree_Node-labels(v) ∈ {L:Atom List| 0 < ||L||}  supposing ↑MTree_Node?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[T:Type].  \mforall{}[v:MultiTree(T)].    MTree\_Node-labels(v)  \mmember{}  \{L:Atom  List|  0  <  ||L||\}    supposing  \muparrow{}MTree\_Nod\000Ce?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index