Nuprl Lemma : es-interface-union_wf

[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].  (X+Y ∈ EClass(A B))


Proof




Definitions occuring in Statement :  es-interface-union: X+Y eclass: EClass(A[eo; e]) uall: [x:A]. B[x] member: t ∈ T union: left right universe: Type
Lemmas :  eclass-compose2_wf eq_int_wf bag-size_wf nat_wf bool_wf eqtt_to_assert assert_of_eq_int single-bag_wf bag-only_wf2 single-valued-bag-if-le1 le_weakening decidable__lt false_wf le_antisymmetry_iff add_functionality_wrt_le add-zero le-add-cancel eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int not-equal-2 empty-bag_wf bag_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].    (X+Y  \mmember{}  EClass(A  +  B))



Date html generated: 2015_07_20-PM-03_19_12
Last ObjectModification: 2015_01_27-PM-10_22_39

Home Index