---

Step * of Lemma remove-repeats-fun-member

∀[A,B:Type].
  ∀eq:EqDecider(B). ∀f:A ⟶ B. ∀L:A List. ∀a:A.
    ((a ∈ remove-repeats-fun(eq;f;L)) ⇐⇒ ∃i:ℕ||L||. ((L[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f L[j]) = (f a) ∈ B)))))
BY
{ (InductionOnList
   THEN RepUR ``remove-repeats-fun`` 0
   THEN Try (Complete ((Auto THEN ExRepD THEN D (-3) THEN Auto)))
   THEN Try (Fold `remove-repeats-fun` 0)
   THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. u : A
6. v : A List
7. ∀a:A. ((a ∈ remove-repeats-fun(eq;f;v)) ⇐⇒ ∃i:ℕ||v||. ((v[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f v[j]) = (f a) ∈ B)))))
8. a : A
9. (a ∈ [u / filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v))])
⊢ ∃i:ℕ||v|| + 1. (([u / v][i] = a ∈ A) ∧ (∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))))

2
1. [A] : Type
2. [B] : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. u : A
6. v : A List
7. ∀a:A. ((a ∈ remove-repeats-fun(eq;f;v)) ⇐⇒ ∃i:ℕ||v||. ((v[i] = a ∈ A) ∧ (∀j:ℕi. (¬((f v[j]) = (f a) ∈ B)))))
8. a : A
9. ∃i:ℕ||v|| + 1. (([u / v][i] = a ∈ A) ∧ (∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))))
⊢ (a ∈ [u / filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v))])

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}eq:EqDecider(B).  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}L:A  List.  \mforall{}a:A.
        ((a  \mmember{}  remove-repeats-fun(eq;f;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||L||.  ((L[i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  L[j])  =  (f  a))))))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``remove-repeats-fun``  0
  THEN  Try  (Complete  ((Auto  THEN  ExRepD  THEN  D  (-3)  THEN  Auto)))
  THEN  Try  (Fold  `remove-repeats-fun`  0)
  THEN  Auto)

---

Home Index