---

Step * of Lemma btr_Node_wf

∀[left,right:binary-tree()].  (btr_Node(left;right) ∈ binary-tree())
BY
{ DepprodCoDatatypeConstructorWf `binary-tree_size` }

---

Latex:


\mforall{}[left,right:binary-tree()].    (btr\_Node(left;right)  \mmember{}  binary-tree())


By

DepprodCoDatatypeConstructorWf  `binary-tree\_size`

---

Home Index