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