Step
*
of Lemma
aa_data_wrapnode_wf
[T:Type]. 
[nd:aa_data_wrapper(T)].  (aa_data_wrapnode(nd) 
 aa_data_wrapper(T))
BY
{ Unfolds ``aa_data_wrapper aa_data_wrapnode`` 0 THEN Auto THEN MemTypeCD THEN Auto }
\mforall{}[T:Type].  \mforall{}[nd:aa\_data\_wrapper(T)].    (aa\_data\_wrapnode(nd)  \mmember{}  aa\_data\_wrapper(T))
By
Unfolds  ``aa\_data\_wrapper  aa\_data\_wrapnode``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto
Home
Index