---

Step * 1 of Lemma member-count-repeats2


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)|| ∈ ℤ
BY
{ ((InstLemma  `apply-alist-count-repeats` [⌜T⌝;⌜eq⌝;⌜v1⌝;⌜L⌝]⋅ THENA Auto) THEN SplitOnHypITE -1  THEN Auto) }

1
.....truecase..... 
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 × ℕ+)
8. apply-alist(eq;count-repeats(L,eq);v1) = (inl ||filter(λy.(eq y v1);L)||) ∈ (ℕ+?)
9. (v1 ∈ L)
⊢ v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ

2
.....falsecase..... 
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 × ℕ+)
8. apply-alist(eq;count-repeats(L,eq);v1) = (inr ⋅ ) ∈ (ℕ+?)
9. ¬(v1 ∈ L)
⊢ v2 = ||filter(λy.(eq y v1);L)|| ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  i  :  \mBbbN{}||count-repeats(L,eq)||
5.  v1  :  T
6.  v2  :  \mBbbN{}\msupplus{}
7.  count-repeats(L,eq)[i]  =  <v1,  v2>
\mvdash{}  v2  =  ||filter(\mlambda{}y.(eq  y  v1);L)||


By

---

Latex:
((InstLemma    `apply-alist-count-repeats`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index