---

Step * of Lemma bag-no-repeats-count

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)].  uiff(bag-no-repeats(T;bs);∀[x:T]. uiff(1 ≤ (#x in bs);(#x in bs) = 1 ∈ ℤ))
BY
{ (Auto THEN Try ((Unhide THEN Auto)) THEN Try ((Unfold `bag-no-repeats` 0 THEN Complete (Auto)))) }

1
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 ∈ ℤ

2
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. ∀[x:T]. uiff(1 ≤ (#x in bs);(#x in bs) = 1 ∈ ℤ)
⊢ bag-no-repeats(T;bs)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].
    uiff(bag-no-repeats(T;bs);\mforall{}[x:T].  uiff(1  \mleq{}  (\#x  in  bs);(\#x  in  bs)  =  1))


By

---

Latex:
(Auto  THEN  Try  ((Unhide  THEN  Auto))  THEN  Try  ((Unfold  `bag-no-repeats`  0  THEN  Complete  (Auto))))

---

Home Index