---

Step * of Lemma btr_Node-left_wf

∀[v:binary-tree()]. btr_Node-left(v) ∈ binary-tree() supposing ↑btr_Node?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:binary-tree()].  btr\_Node-left(v)  \mmember{}  binary-tree()  supposing  \muparrow{}btr\_Node?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index