---

Step * 2 1 1 of Lemma remove-repeats-fun-member


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
10. v[i - 1] = a ∈ A
11. ∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))
12. ¬(i = 0 ∈ ℤ)
13. ¬((f u) = (f a) ∈ B)
⊢ (a ∈ remove-repeats-fun(eq;f;v))
BY
{ (BackThruSomeHyp
   THEN (InstConcl [⌜i - 1⌝]⋅ THEN Auto)
   THEN (InstHyp [⌜j + 1⌝] (-5)⋅ THENA Auto)
   THEN RWO "select_cons_tl" (-1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  eq  :  EqDecider(B)
4.  f  :  A  {}\mrightarrow{}  B
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}a:A
          ((a  \mmember{}  remove-repeats-fun(eq;f;v))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((v[i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  v[j])  =  (f  a))))))
8.  a  :  A
9.  i  :  \mBbbN{}||v||  +  1
10.  v[i  -  1]  =  a
11.  \mforall{}j:\mBbbN{}i.  (\mneg{}((f  [u  /  v][j])  =  (f  a)))
12.  \mneg{}(i  =  0)
13.  \mneg{}((f  u)  =  (f  a))
\mvdash{}  (a  \mmember{}  remove-repeats-fun(eq;f;v))


By

---

Latex:
(BackThruSomeHyp
  THEN  (InstConcl  [\mkleeneopen{}i  -  1\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}j  +  1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  RWO  "select\_cons\_tl"  (-1)
  THEN  Auto)\mcdot{}

---

Home Index