Nuprl Lemma : aa_lt_node?_wf
[T:Type]. [x:aa_ltree(T)]. (aa_lt_node?(x) 
)
Proof
Definitions occuring in Statement :
aa_lt_node?: aa_lt_node?(x),
aa_ltree: aa_ltree(T),
bool: ,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
aa_lt_node?: aa_lt_node?(x),
so_lambda: so_lambda(x,y,z,w,v.t[x; y; z; w; v]),
so_apply: x[s1;s2;s3;s4;s5]
Lemmas :
aa_ltree_ind_wf,
bool_wf,
bfalse_wf,
btrue_wf,
aa_ltree_wf,
subtype_rel_self
\mforall{}[T:Type]. \mforall{}[x:aa\_ltree(T)]. (aa\_lt\_node?(x) \mmember{} \mBbbB{})
Date html generated:
2013_03_20-AM-10_58_02
Last ObjectModification:
2012_11_27-AM-10_32_35
Home
Index