Step
*
of Lemma
MTree_Node-children_wf
∀[T:Type]. ∀[v:MultiTree(T)]. MTree_Node-children(v) ∈ {a:Atom| (a ∈ MTree_Node-labels(v))} ─→ MultiTree(T) supposing \000C↑MTree_Node?(v)
BY
{ DepprodCoDatatypeSelectorWf }
Latex:
\mforall{}[T:Type]. \mforall{}[v:MultiTree(T)].
MTree\_Node-children(v) \mmember{} \{a:Atom| (a \mmember{} MTree\_Node-labels(v))\} {}\mrightarrow{} MultiTree(T) supposing \muparrow{}MTree\_No\000Cde?(v)
By
DepprodCoDatatypeSelectorWf
Home
Index