---

Step * 2 1 of Lemma remove-repeats_property


1. [T] : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. no_repeats(T;remove-repeats(eq;v))
6. ∀a:T. ((a ∈ remove-repeats(eq;v)) ⇐⇒ (a ∈ v))
7. no_repeats(T;[u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
8. a : T
9. (a ∈ filter(λx.(¬b(eq x u));remove-repeats(eq;v)))
⊢ (a ∈ v)
BY
{ (RWO "member_filter" (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  no\_repeats(T;remove-repeats(eq;v))
6.  \mforall{}a:T.  ((a  \mmember{}  remove-repeats(eq;v))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  v))
7.  no\_repeats(T;[u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))])
8.  a  :  T
9.  (a  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v)))
\mvdash{}  (a  \mmember{}  v)


By

---

Latex:
(RWO  "member\_filter"  (-1)  THEN  Auto)\mcdot{}

---

Home Index