---

Step * of Lemma member-count-repeats1

∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:T List.  ((x ∈ map(λp.(fst(p));count-repeats(L,eq))) ⇐⇒ (x ∈ L))
BY
{ ((InstLemma  `apply-alist-count-repeats` [] THEN RepeatFor 4 (ParallelLast')) THEN SplitOnHypITE -1  THEN Auto) }

1
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)))

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.    ((x  \mmember{}  map(\mlambda{}p.(fst(p));count-repeats(L,eq)))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
((InstLemma    `apply-alist-count-repeats`  []  THEN  RepeatFor  4  (ParallelLast'))
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index