### Nuprl Lemma : reverse-bag

`∀[T:Type]. ∀[b:bag(T)].  (rev(b) = b ∈ bag(T))`

Proof

Definitions occuring in Statement :  bag: `bag(T)` reverse: `rev(as)` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = 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: `P `` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` prop: `ℙ` guard: `{T}`
Lemmas referenced :  list_wf quotient-member-eq permutation_wf permutation-equiv reverse_wf equal_wf equal-wf-base bag_wf permutation-reverse permutation_inversion permutation_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination cumulativity hypothesisEquality lambdaFormation rename lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination productEquality isect_memberEquality axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    (rev(b)  =  b)

Date html generated: 2017_10_01-AM-08_44_58
Last ObjectModification: 2017_07_26-PM-04_30_27

Theory : bags

Home Index