---

Step * of Lemma btr_Node-right_wf

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

---

Latex:


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


By

DepprodCoDatatypeSelectorWf

---

Home Index