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