---

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


1. T : Type
2. eq : EqDecider(T)
3. bs : T List
4. ∀[x:T]. uiff(1 ≤ count(eq x;bs);count(eq x;bs) = 1 ∈ ℤ)
5. ∀[x:T]. uiff(1 ≤ ||filter(λy.(eq x y);bs)||;||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ)
6. bs = bs ∈ bag(T)
7. x : T
8. 1 ≤ ||filter(eq x;bs)||
9. 1 ≤ ||filter(λy.(eq x y);bs)|| supposing ||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ
10. ||filter(λy.(eq x y);bs)|| = 1 ∈ ℤ
⊢ ||filter(eq x;bs)|| = 1 ∈ ℤ
BY
{ ((NthHypEq (-1) THEN RepeatFor 3 ((EqCD THEN Auto))) THEN Ext THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  T  List
4.  \mforall{}[x:T].  uiff(1  \mleq{}  count(eq  x;bs);count(eq  x;bs)  =  1)
5.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);bs)||;||filter(\mlambda{}y.(eq  x  y);bs)||  =  1)
6.  bs  =  bs
7.  x  :  T
8.  1  \mleq{}  ||filter(eq  x;bs)||
9.  1  \mleq{}  ||filter(\mlambda{}y.(eq  x  y);bs)||  supposing  ||filter(\mlambda{}y.(eq  x  y);bs)||  =  1
10.  ||filter(\mlambda{}y.(eq  x  y);bs)||  =  1
\mvdash{}  ||filter(eq  x;bs)||  =  1


By

---

Latex:
((NthHypEq  (-1)  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))  THEN  Ext  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index