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

`∀[T,A:Type]. ∀[bs:bag(A)].  (bag-no-repeats(A;bs)) supposing (bag-no-repeats(T;bs) and strong-subtype(A;T))`

Proof

Definitions occuring in Statement :  bag-no-repeats: `bag-no-repeats(T;bs)` bag: `bag(T)` strong-subtype: `strong-subtype(A;B)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` exists: `∃x:A. B[x]` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B` strong-subtype: `strong-subtype(A;B)` cand: `A c∧ B` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_stable: `SqStable(P)` bag: `bag(T)` quotient: `x,y:A//B[x; y]` permutation: `permutation(T;L1;L2)` guard: `{T}`
Lemmas referenced :  bag-no-repeats_wf subtype_rel_bag strong-subtype_wf bag_wf list_wf equal_wf list-subtype-bag squash_wf exists_wf subtype_rel_list all_wf bag_to_squash_list sq_stable__all sq_stable__squash member_wf permutation_wf permute_list_wf int_seg_wf length_wf strong-subtype-list strong-subtype-implies no_repeats-subtype no_repeats_wf strong-subtype-bag
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution imageElimination productElimination thin sqequalRule imageMemberEquality hypothesisEquality baseClosed hypothesis extract_by_obid isectElimination cumulativity applyEquality independent_isectElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination independent_functionElimination lambdaEquality functionEquality lambdaFormation promote_hyp rename hyp_replacement applyLambdaEquality pertypeElimination productEquality dependent_pairFormation functionExtensionality natural_numberEquality independent_pairFormation dependent_set_memberEquality setElimination

Latex:
\mforall{}[T,A:Type].  \mforall{}[bs:bag(A)].
(bag-no-repeats(A;bs))  supposing  (bag-no-repeats(T;bs)  and  strong-subtype(A;T))

Date html generated: 2017_10_01-AM-08_57_08
Last ObjectModification: 2017_07_26-PM-04_39_17

Theory : bags

Home Index