Nuprl Lemma : aa_ltree_wf
[T:Type]. (aa_ltree(T) 
Type)
Proof
Definitions occuring in Statement :
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),
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a
Lemmas :
unit_wf2,
subtype_rel_sum,
subtype_rel_simple_product
\mforall{}[T:Type]. (aa\_ltree(T) \mmember{} Type)
Date html generated:
2013_03_20-AM-10_57_33
Last ObjectModification:
2012_11_27-AM-10_32_19
Home
Index