---

Step * of Lemma binary-tree_size_wf

∀[p:binary-tree()]. (binary-tree_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `binary-treeco_size` }

---

Latex:


\mforall{}[p:binary-tree()].  (binary-tree\_size(p)  \mmember{}  \mBbbN{})


By

ProveCoSizeWf2  `binary-treeco\_size`

---

Home Index