### Nuprl Lemma : bag-extensionality-no-repeats

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀[as,bs:bag(T)].`
`        uiff(as = bs ∈ bag(T);∀x:T. uiff(x ↓∈ as;x ↓∈ bs)) supposing bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs)))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` decidable: `Dec(P)` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` all: `∀x:A. B[x]` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bag-member: `x ↓∈ bs` exists: `∃x:A. B[x]` bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  bag-member_wf squash_wf true_wf bag_wf istype-universe subtype_rel_self iff_weakening_equal bag-no-repeats_wf decidable_wf equal_wf bag_to_squash_list uiff_wf list-subtype-bag quotient-member-eq list_wf permutation_wf permutation-equiv permutation-when-no_repeats l_member_wf no_repeats_functionality_wrt_permutation permutation_inversion respects-equality-list-bag respects-equality-trivial bag-member-list-member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt sqequalHypSubstitution productElimination thin independent_pairFormation applyEquality lambdaEquality_alt imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeIsType instantiate universeEquality natural_numberEquality sqequalRule imageMemberEquality baseClosed because_Cache independent_isectElimination independent_functionElimination dependent_functionElimination independent_pairEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType functionIsTypeImplies equalityIstype functionIsType productIsType isectIsType axiomEquality promote_hyp hyp_replacement applyLambdaEquality functionEquality rename pertypeElimination dependent_pairFormation_alt

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}[as,bs:bag(T)].
uiff(as  =  bs;\mforall{}x:T.  uiff(x  \mdownarrow{}\mmember{}  as;x  \mdownarrow{}\mmember{}  bs))
supposing  bag-no-repeats(T;as)  \mwedge{}  bag-no-repeats(T;bs)))

Date html generated: 2020_05_20-AM-08_02_16
Last ObjectModification: 2020_01_04-PM-10_19_37

Theory : bags

Home Index