---

Step * 3 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 ∈ [u / v])
⊢ (a ∈ [u / filter(λx.(¬b(eq x u));remove-repeats(eq;v))])
BY
{ (All (RWO "cons_member") THEN Auto) }

1
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 = u ∈ T) ∨ (a ∈ v)
⊢ (a = u ∈ T) ∨ (a ∈ filter(λx.(¬b(eq x u));remove-repeats(eq;v)))

---

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{}  [u  /  v])
\mvdash{}  (a  \mmember{}  [u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  u));remove-repeats(eq;v))])


By

---

Latex:
(All  (RWO  "cons\_member")  THEN  Auto)

---

Home Index