---

Step * 2 of Lemma member-count-repeats1


1. [T] : Type
2. eq : EqDecider(T)@i
3. x : T@i
4. L : T List@i
5. apply-alist(eq;count-repeats(L,eq);x) = (inr ⋅ ) ∈ (ℕ+?)
6. ¬(x ∈ L)
7. (x ∈ map(λp.(fst(p));count-repeats(L,eq)))@i
⊢ (x ∈ L)
BY
{ (Using [`eq',⌜eq⌝] (FLemma `isl-apply-alist` [-1])⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)@i
3.  x  :  T@i
4.  L  :  T  List@i
5.  apply-alist(eq;count-repeats(L,eq);x)  =  (inr  \mcdot{}  )
6.  \mneg{}(x  \mmember{}  L)
7.  (x  \mmember{}  map(\mlambda{}p.(fst(p));count-repeats(L,eq)))@i
\mvdash{}  (x  \mmember{}  L)


By

---

Latex:
(Using  [`eq',\mkleeneopen{}eq\mkleeneclose{}]  (FLemma  `isl-apply-alist`  [-1])\mcdot{}  THEN  Auto)

---

Home Index