---

Step * 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. (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))))
BY
{ ((RW ListC (-1) THENA Auto)
   THEN D (-1)
   THEN Try (Complete ((InstConcl [⌜0⌝]⋅ THEN Reduce 0 THEN Auto)))
   THEN (RW ListC (-1) THENA Auto)
   THEN Reduce (-1)
   THEN RepD
   THEN (FHyp (-4) [-2] THENA Auto)
   THEN ExRepD
   THEN (RW assert_pushdownC (-4) THENA 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 ∈ remove-repeats-fun(eq;f;v))
10. ¬((f a) = (f u) ∈ B)
11. i : ℕ||v||
12. v[i] = a ∈ A
13. ∀j:ℕi. (¬((f v[j]) = (f a) ∈ B))
⊢ ∃i:ℕ||v|| + 1. (([u / v][i] = a ∈ A) ∧ (∀j:ℕi. (¬((f [u / v][j]) = (f a) ∈ B))))

---

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.  (a  \mmember{}  [u  /  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  u)));remove-repeats-fun(eq;f;v))])
\mvdash{}  \mexists{}i:\mBbbN{}||v||  +  1.  (([u  /  v][i]  =  a)  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}((f  [u  /  v][j])  =  (f  a)))))


By

---

Latex:
((RW  ListC  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  ((InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)))
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RepD
  THEN  (FHyp  (-4)  [-2]  THENA  Auto)
  THEN  ExRepD
  THEN  (RW  assert\_pushdownC  (-4)  THENA  Auto))

---

Home Index