Nuprl Lemma : aa_lt_leaf_wf
[T:Type]. (aa_lt_leaf()  aa_ltree(T))
Proof
Definitions occuring in Statement : 
aa_lt_leaf: aa_lt_leaf(), 
aa_ltree: aa_ltree(T), 
uall: [x:A]. B[x], 
member: t  T, 
universe: Type
Definitions : 
uall: [x:A]. B[x], 
member: t  T, 
aa_ltree: aa_ltree(T), 
aa_lt_leaf: aa_lt_leaf(), 
type-monotone: Monotone(T.F[T]), 
uimplies: b supposing a
Lemmas : 
it_wf, 
unit_wf2, 
subtype_rel_sum, 
subtype_rel_simple_product, 
subtype_rel_self
\mforall{}[T:Type].  (aa\_lt\_leaf()  \mmember{}  aa\_ltree(T))
Date html generated:
2013_03_20-AM-10_57_37
Last ObjectModification:
2012_11_27-AM-10_32_20
Home
Index