Step
*
of Lemma
aa_wrapper_get_data_wf
T:Type.
dw:aa_data_wrapper(T).
(aa_wrapper_get_data(dw)
T)
BY
{
ProveWfLemma
}
\mforall{}T:Type. \mforall{}dw:aa\_data\_wrapper(T). (aa\_wrapper\_get\_data(dw) \mmember{} T)
By
ProveWfLemma
Home
Index
T:Type. dw:aa_data_wrapper(T). (aa_wrapper_get_data(dw) 
T)