---

Step * of Lemma l_tree_node_wf

∀[L,T:Type]. ∀[val:T]. ∀[left_subtree,right_subtree:l_tree(L;T)].
  (l_tree_node(val;left_subtree;right_subtree) ∈ l_tree(L;T))
BY
{ DepprodCoDatatypeConstructorWf `l_tree_size` }

---

Latex:

---

Latex:
\mforall{}[L,T:Type].  \mforall{}[val:T].  \mforall{}[left$_{subtree}$,right$_{subtree}$:\000Cl\_tree(L;T)].
    (l\_tree\_node(val;left$_{subtree}$;right$_{subtree}$)  \mmember{}  l\_t\000Cree(L;T))


By

---

Latex:
DepprodCoDatatypeConstructorWf  `l\_tree\_size`

---

Home Index