---

Step * of Lemma btr_Leaf_wf

∀[val:ℤ]. (btr_Leaf(val) ∈ binary-tree())
BY
{ DepprodCoDatatypeConstructorWf `binary-tree_size` }

---

Latex:


\mforall{}[val:\mBbbZ{}].  (btr\_Leaf(val)  \mmember{}  binary-tree())


By

DepprodCoDatatypeConstructorWf  `binary-tree\_size`

---

Home Index