Nuprl Lemma : bag-append-comm

[T:Type]. ∀[as,bs:bag(T)].  ((as bs) (bs as) ∈ bag(T))


Proof




Definitions occuring in Statement :  bag-append: as bs bag: bag(T) uall: [x:A]. B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag: bag(T) quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] implies:  Q bag-append: as bs so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a iff: ⇐⇒ Q rev_implies:  Q prop:
Lemmas referenced :  quotient-member-eq list_wf permutation_wf permutation-equiv append_wf permutation_functionality_wrt_permutation permutation_weakening append_functionality_wrt_permutation permutation_inversion permutation-rotate bag_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache hypothesis sqequalRule pertypeElimination promote_hyp thin productElimination equalityTransitivity equalitySymmetry inhabitedIsType lambdaFormation_alt rename extract_by_obid isectElimination hypothesisEquality lambdaEquality_alt independent_isectElimination dependent_functionElimination independent_functionElimination universeIsType equalityIstype productIsType sqequalBase isect_memberEquality_alt axiomEquality isectIsTypeImplies instantiate universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].    ((as  +  bs)  =  (bs  +  as))



Date html generated: 2020_05_20-AM-08_01_29
Last ObjectModification: 2020_01_04-PM-11_16_43

Theory : bags


Home Index