---

Step * of Lemma aa_lt_node-right_subtree_wf

[T:Type]. [x:aa_ltree(T)].  aa_lt_node-right_subtree(x)  aa_ltree(T) supposing aa_lt_node?(x)
BY
{ DatatypeSelectorWf `` aa_lt_leaf aa_lt_node`` }


\mforall{}[T:Type].  \mforall{}[x:aa\_ltree(T)].    aa\_lt\_node-right\_subtree(x)  \mmember{}  aa\_ltree(T)  supposing  \muparrow{}aa\_lt\_node?(x)


By

DatatypeSelectorWf  ``  aa\_lt\_leaf  aa\_lt\_node``



Home Index