Nuprl Lemma : aa_data_wrapnode_wf
[T:Type]. [nd:aa_data_wrapper(T)]. (aa_data_wrapnode(nd) 
aa_data_wrapper(T))
Proof
Definitions occuring in Statement :
aa_data_wrapnode: aa_data_wrapnode(nd),
aa_data_wrapper: aa_data_wrapper(T),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
aa_data_wrapper: aa_data_wrapper(T),
member: t T,
aa_data_wrapnode: aa_data_wrapnode(nd),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
guard: {T}
Lemmas :
subtype_rel_sum,
subtype_rel_self
\mforall{}[T:Type]. \mforall{}[nd:aa\_data\_wrapper(T)]. (aa\_data\_wrapnode(nd) \mmember{} aa\_data\_wrapper(T))
Date html generated:
2013_03_20-AM-11_02_24
Last ObjectModification:
2012_11_27-AM-10_33_04
Home
Index