---

Step * 1 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 : A
14. (x ∈ v)
15. ↑R[x;u]
16. (f x) = (f u) ∈ B
⊢ False
BY
{ ((RWO "l_all_iff" (-6) THENA Auto)
   THEN (InstHyp [⌜x⌝] (-6)⋅ THEN Auto)
   THEN UnfoldTopAb (-9)
   THEN InstHyp [⌜u⌝;⌜x⌝] (-9)⋅
   THEN Auto) }

---

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.  x  :  A
14.  (x  \mmember{}  v)
15.  \muparrow{}R[x;u]
16.  (f  x)  =  (f  u)
\mvdash{}  False


By

---

Latex:
((RWO  "l\_all\_iff"  (-6)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)
  THEN  UnfoldTopAb  (-9)
  THEN  InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-9)\mcdot{}
  THEN  Auto)

---

Home Index