---

Step * of Lemma aa_data_wrapper_wf

[T:Type]. (aa_data_wrapper(T)  Type)
BY
{ Unfold `aa_data_wrapper` 0 THEN Auto }


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


By

Unfold  `aa\_data\_wrapper`  0  THEN  Auto



Home Index