---

Step * 1 of Lemma bag-no-repeats-count


1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. bag-no-repeats(T;bs)
5. x : T
6. 1 ≤ (#x in bs)
⊢ (#x in bs) = 1 ∈ ℤ
BY
{ (All (RWO "bag-count-sqequal") THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. bag-no-repeats(T;bs)
5. x : T
6. 1 ≤ #([y∈bs|eq x y])
⊢ #([y∈bs|eq x y]) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  bag-no-repeats(T;bs)
5.  x  :  T
6.  1  \mleq{}  (\#x  in  bs)
\mvdash{}  (\#x  in  bs)  =  1


By

---

Latex:
(All  (RWO  "bag-count-sqequal")  THEN  Auto)

---

Home Index