Nuprl Lemma : aa_wrapper_get_data_wf
T:Type. dw:aa_data_wrapper(T). (aa_wrapper_get_data(dw) 
T)
Proof
Definitions occuring in Statement :
aa_wrapper_get_data: aa_wrapper_get_data(dw),
aa_data_wrapper: aa_data_wrapper(T),
all: x:A. B[x],
member: t T,
universe: Type
Definitions :
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
aa_wrapper_get_data: aa_wrapper_get_data(dw),
member: t T,
all: x:A. B[x],
so_apply: x[s],
so_apply: x[s1;s2],
uall: [x:A]. B[x]
Lemmas :
aa_data_wrapper_wf,
aa_data_wrapper_ind_wf
\mforall{}T:Type. \mforall{}dw:aa\_data\_wrapper(T). (aa\_wrapper\_get\_data(dw) \mmember{} T)
Date html generated:
2013_03_20-AM-11_02_35
Last ObjectModification:
2012_11_27-AM-10_33_12
Home
Index