Nuprl Lemma : RankEx1_ProdL_wf

[T:Type]. ∀[prodl:T × RankEx1(T)].  (RankEx1_ProdL(prodl) ∈ RankEx1(T))


Proof




Definitions occuring in Statement :  RankEx1_ProdL: RankEx1_ProdL(prodl) RankEx1: RankEx1(T) uall: [x:A]. B[x] member: t ∈ T product: x:A × B[x] universe: Type
Lemmas :  RankEx1co-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 RankEx1co_wf list_wf add_nat_wf false_wf le_wf RankEx1_size_wf nat_wf value-type-has-value set-value-type int-value-type has-value_wf-partial RankEx1co_size_wf RankEx1_wf
\mforall{}[T:Type].  \mforall{}[prodl:T  \mtimes{}  RankEx1(T)].    (RankEx1\_ProdL(prodl)  \mmember{}  RankEx1(T))



Date html generated: 2015_07_17-AM-07_47_50
Last ObjectModification: 2015_01_27-AM-09_38_37

Home Index