---

Step * of Lemma member-count-repeats2

∀[T:Type]
  ∀eq:EqDecider(T). ∀L:T List. ∀i:ℕ||count-repeats(L,eq)||.
    let x,n = count-repeats(L,eq)[i] 
    in n = ||filter(λy.(eq y x);L)|| ∈ ℤ
BY
{ (Auto THEN GenConclAtAddr [1] THEN D -2 THEN Reduce 0) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. i : ℕ||count-repeats(L,eq)||
5. v1 : T
6. v2 : ℕ+
7. count-repeats(L,eq)[i] = <v1, v2> ∈ (T × ℕ+)
⊢ v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||count-repeats(L,eq)||.
        let  x,n  =  count-repeats(L,eq)[i] 
        in  n  =  ||filter(\mlambda{}y.(eq  y  x);L)||


By

---

Latex:
(Auto  THEN  GenConclAtAddr  [1]  THEN  D  -2  THEN  Reduce  0)

---

Home Index