---

Step * of Lemma aa_data_wrapleaf-val_wf

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


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


By

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



Home Index