Nuprl Lemma : product-equipollent-tuple3

L:Type List. ∀[A:Type]. tuple-type(L) × tuple-type(L [A])


Proof




Definitions occuring in Statement :  equipollent: B tuple-type: tuple-type(L) append: as bs cons: [a b] nil: [] list: List uall: [x:A]. B[x] all: x:A. B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] subtype_rel: A ⊆B prop: so_apply: x[s] implies:  Q append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] ifthenelse: if then else fi  btrue: tt or: P ∨ Q cons: [a b] uimplies: supposing a bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) and: P ∧ Q bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A rev_implies:  Q iff: ⇐⇒ Q nat:
Lemmas referenced :  list_induction uall_wf equipollent_wf tuple-type_wf append_wf cons_wf nil_wf tupletype_nil_lemma list_ind_nil_lemma istype-void tupletype_cons_lemma null_nil_lemma list_ind_cons_lemma list_wf equipollent-identity unit_wf2 equipollent_same list-cases null_cons_lemma product_subtype_list null_wf3 subtype_rel_list top_wf eqtt_to_assert assert_of_null eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base length_wf_nat nat_wf set_subtype_base le_wf istype-int int_subtype_base equipollent_weakening_ext-eq ext-eq_weakening equipollent_functionality_wrt_equipollent2 product_functionality_wrt_equipollent_right equipollent_inversion equipollent-product-assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination universeEquality sqequalRule lambdaEquality_alt productEquality hypothesisEquality hypothesis applyEquality cumulativity inhabitedIsType equalityTransitivity equalitySymmetry because_Cache universeIsType independent_functionElimination dependent_functionElimination isect_memberEquality_alt voidElimination rename isectIsType isect_memberFormation_alt unionElimination promote_hyp hypothesis_subsumption productElimination independent_isectElimination equalityElimination dependent_pairFormation_alt equalityIsType1 baseClosed equalityIsType3 dependent_set_memberEquality_alt equalityIsType4 intEquality natural_numberEquality hyp_replacement applyLambdaEquality setElimination

Latex:
\mforall{}L:Type  List.  \mforall{}[A:Type].  tuple-type(L)  \mtimes{}  A  \msim{}  tuple-type(L  @  [A])



Date html generated: 2019_10_15-AM-11_15_23
Last ObjectModification: 2018_10_09-PM-02_12_44

Theory : general


Home Index