---

Step * of Lemma l_tree_leaf_wf

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

---

Latex:


\mforall{}[L,T:Type].  \mforall{}[val:L].    (l\_tree\_leaf(val)  \mmember{}  l\_tree(L;T))


By

DepprodCoDatatypeConstructorWf  `l\_tree\_size`

---

Home Index