---

Step * 1 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) = (inl ||filter(λy.(eq y x);L)||) ∈ (ℕ+?)
6. (x ∈ L)
7. (x ∈ L)@i
⊢ (x ∈ map(λp.(fst(p));count-repeats(L,eq)))
BY
{ (Using [`eq',⌜eq⌝] (BLemma `isl-apply-alist`)⋅ 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)  =  (inl  ||filter(\mlambda{}y.(eq  y  x);L)||)
6.  (x  \mmember{}  L)
7.  (x  \mmember{}  L)@i
\mvdash{}  (x  \mmember{}  map(\mlambda{}p.(fst(p));count-repeats(L,eq)))


By

---

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

---

Home Index