---

Step * of Lemma aa_data_wrapleaf_wf

[T:Type]. [val:T].  (aa_data_wrapleaf(val)  aa_data_wrapper(T))
BY
{ Unfolds ``aa_data_wrapper aa_data_wrapleaf`` 0 THEN Auto THEN MemTypeCD THEN Auto }


\mforall{}[T:Type].  \mforall{}[val:T].    (aa\_data\_wrapleaf(val)  \mmember{}  aa\_data\_wrapper(T))


By

Unfolds  ``aa\_data\_wrapper  aa\_data\_wrapleaf``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto



Home Index