---

Step * of Lemma aa_lt_node-val_wf

[T:Type]. [x:aa_ltree(T)].  aa_lt_node-val(x)  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-val(x)  \mmember{}  T  supposing  \muparrow{}aa\_lt\_node?(x)


By

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



Home Index