---

Step * of Lemma aa_data_wrapnode-nd_wf

[T:Type]. [x:aa_data_wrapper(T)].  aa_data_wrapnode-nd(x)  aa_data_wrapper(T) supposing aa_data_wrapnode?(x)
BY
{ DatatypeSelectorWf `` aa_data_wrapnode aa_data_wrapleaf`` }


\mforall{}[T:Type].  \mforall{}[x:aa\_data\_wrapper(T)].
    aa\_data\_wrapnode-nd(x)  \mmember{}  aa\_data\_wrapper(T)  supposing  \muparrow{}aa\_data\_wrapnode?(x)


By

DatatypeSelectorWf  ``  aa\_data\_wrapnode  aa\_data\_wrapleaf``



Home Index