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