### Nuprl Lemma : respects-equality-bag

`∀[A,B:Type].  respects-equality(bag(A);bag(B)) supposing respects-equality(A;B)`

Proof

Definitions occuring in Statement :  bag: `bag(T)` uimplies: `b supposing a` respects-equality: `respects-equality(S;T)` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` bag: `bag(T)` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` permutation: `permutation(T;L1;L2)` exists: `∃x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` prop: `ℙ` respects-equality: `respects-equality(S;T)` label: `...\$L... t` guard: `{T}` surject: `Surj(A;B;f)` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` permute_list: `(L o f)`
Lemmas referenced :  respects-equality-quotient list_wf permutation_wf permutation-equiv respects-equality-list respects-equality_wf istype-universe permutation_inversion change-equality-type inject_wf int_seg_wf length_wf permute_list_wf respects-equality-list-type injection-is-surjection length_wf_nat int_seg_properties decidable__equal_int full-omega-unsat intformand_wf intformnot_wf intformeq_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf set_subtype_base lelt_wf int_subtype_base subtype_base_sq select_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma permutation-length equal_wf squash_wf true_wf subtype_rel_self iff_weakening_equal decidable__lt intformless_wf int_formula_prop_less_lemma select-mklist
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality_alt inhabitedIsType universeIsType because_Cache independent_isectElimination lambdaFormation_alt instantiate universeEquality dependent_functionElimination independent_functionElimination productElimination equalityTransitivity equalitySymmetry dependent_pairFormation_alt independent_pairFormation productIsType natural_numberEquality equalityIstype applyLambdaEquality setElimination rename unionElimination approximateComputation int_eqEquality isect_memberEquality_alt voidElimination applyEquality intEquality closedConclusion sqequalBase cumulativity dependent_set_memberEquality_alt imageElimination imageMemberEquality baseClosed functionExtensionality

Latex:
\mforall{}[A,B:Type].    respects-equality(bag(A);bag(B))  supposing  respects-equality(A;B)

Date html generated: 2019_10_15-AM-10_59_48
Last ObjectModification: 2018_11_29-PM-07_12_40

Theory : bags

Home Index