Nuprl Lemma : RankEx2_LeafT_wf

[S,T:Type]. ∀[leaft:T].  (RankEx2_LeafT(leaft) ∈ RankEx2(S;T))


Proof




Definitions occuring in Statement :  RankEx2_LeafT: RankEx2_LeafT(leaft) RankEx2: RankEx2(S;T) uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  RankEx2co-ext eq_atom_wf bool_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom eqtt_to_assert assert_of_eq_atom RankEx2co_wf list_wf false_wf le_wf nat_wf has-value_wf_base set_subtype_base int_subtype_base has-value_wf-partial set-value-type int-value-type RankEx2co_size_wf
\mforall{}[S,T:Type].  \mforall{}[leaft:T].    (RankEx2\_LeafT(leaft)  \mmember{}  RankEx2(S;T))



Date html generated: 2015_07_17-AM-07_49_06
Last ObjectModification: 2015_01_27-AM-09_38_05

Home Index