---

Step * 2 of Lemma bag-member-count


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. 1 ≤ #([y∈bs|eq x y])
⊢ x ↓∈ bs
BY
{ (MoveToConcl (-1) THEN UseWitness ⌜λh.Ax⌝⋅ THEN (Unfold `bag` 4 THEN newQuotientElim 4) THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. T List ∈ Type
5. ∀as,b1:T List.  (permutation(T;as;b1) ∈ Type)
6. ∀as:T List. permutation(T;as;as)
7. as : T List
8. b1 : T List
9. permutation(T;as;b1)
10. ((1 ≤ #([y∈as|eq x y])) ⇒ x ↓∈ as) = ((1 ≤ #([y∈b1|eq x y])) ⇒ x ↓∈ b1) ∈ Type
11. h : 1 ≤ #([y∈as|eq x y])
⊢ Ax ∈ x ↓∈ as

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  bs  :  bag(T)
5.  1  \mleq{}  \#([y\mmember{}bs|eq  x  y])
\mvdash{}  x  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(MoveToConcl  (-1)  THEN  UseWitness  \mkleeneopen{}\mlambda{}h.Ax\mkleeneclose{}\mcdot{}  THEN  (Unfold  `bag`  4  THEN  newQuotientElim  4)  THEN  Auto)

---

Home Index