---

Step * 1 of Lemma remove-repeats-fun-as-filter


1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. R : A ⟶ A ⟶ 𝔹
6. u : A
7. v : A List
8. Irrefl(A;x,y.↑R[x;y])
9. StAntiSym(A;x,y.↑R[x;y])
10. sorted-by(λx,y. (↑R[x;y]);v)
11. (∀z∈v.↑R[u;z])
12. remove-repeats-fun(eq;f;v) ~ filter(λa.(¬b(∃x∈v.R[x;a] ∧b (eq (f x) (f a)))_b);v)
13. (∃x∈[u / v]. (↑R[x;u]) ∧ ((f x) = (f u) ∈ B))
⊢ [u / filter(λt.((¬b(∃x∈v.R[x;t] ∧b (eq (f x) (f t)))_b) ∧b (¬b(eq (f t) (f u))));v)] ~ filter(λa.(¬b(∃x∈[u / v].R[x;a]
                                                                                                         ∧b (eq (f x) 
                                                                                                             (f a)))_b);
                                                                                                v)
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD
   THEN (RW ListC (-3) THENA Auto)
   THEN D (-3)
   THEN Auto) }

1
1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. R : A ⟶ A ⟶ 𝔹
6. u : A
7. v : A List
8. Irrefl(A;x,y.↑R[x;y])
9. StAntiSym(A;x,y.↑R[x;y])
10. sorted-by(λx,y. (↑R[x;y]);v)
11. (∀z∈v.↑R[u;z])
12. remove-repeats-fun(eq;f;v) ~ filter(λa.(¬b(∃x∈v.R[x;a] ∧b (eq (f x) (f a)))_b);v)
13. x : A
14. (x ∈ v)
15. ↑R[x;u]
16. (f x) = (f u) ∈ B
⊢ False

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  eq  :  EqDecider(B)
4.  f  :  A  {}\mrightarrow{}  B
5.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
6.  u  :  A
7.  v  :  A  List
8.  Irrefl(A;x,y.\muparrow{}R[x;y])
9.  StAntiSym(A;x,y.\muparrow{}R[x;y])
10.  sorted-by(\mlambda{}x,y.  (\muparrow{}R[x;y]);v)
11.  (\mforall{}z\mmember{}v.\muparrow{}R[u;z])
12.  remove-repeats-fun(eq;f;v)  \msim{}  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}v.R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);v)
13.  (\mexists{}x\mmember{}[u  /  v].  (\muparrow{}R[x;u])  \mwedge{}  ((f  x)  =  (f  u)))
\mvdash{}  [u  /  filter(\mlambda{}t.((\mneg{}\msubb{}(\mexists{}x\mmember{}v.R[x;t]  \mwedge{}\msubb{}  (eq  (f  x)  (f  t)))\_b)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  (f  t)  (f  u))));v)] 
\msim{}  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}[u  /  v].R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);v)


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RW  ListC  (-3)  THENA  Auto)
  THEN  D  (-3)
  THEN  Auto)

---

Home Index