---

Step * 3 2 of Lemma apply-alist-count-repeats


1. T : Type
2. eq : EqDecider(T)
3. x : T
4. ys : T List@i
5. ¬(x ∈ ys)
6. y : T@i
7. ¬(y = x ∈ T)
8. (x ∈ ys @ [y])
9. 0 < ||filter(λy.(eq y x);ys @ [y])||
10. apply-alist(eq;count-repeats(ys,eq);x) = (inr ⋅ ) ∈ (ℕ+?)
⊢ (inr ⋅ ) = (inl (||filter(λy.(eq y x);ys)|| + 0)) ∈ (ℕ+?)
BY
{ ((RWW "member_append member_singleton" (-3) THENM D -3) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
4.  ys  :  T  List@i
5.  \mneg{}(x  \mmember{}  ys)
6.  y  :  T@i
7.  \mneg{}(y  =  x)
8.  (x  \mmember{}  ys  @  [y])
9.  0  <  ||filter(\mlambda{}y.(eq  y  x);ys  @  [y])||
10.  apply-alist(eq;count-repeats(ys,eq);x)  =  (inr  \mcdot{}  )
\mvdash{}  (inr  \mcdot{}  )  =  (inl  (||filter(\mlambda{}y.(eq  y  x);ys)||  +  0))


By

---

Latex:
((RWW  "member\_append  member\_singleton"  (-3)  THENM  D  -3)  THEN  Auto)\mcdot{}

---

Home Index