---

Step * of Lemma l-ordered-remove-repeats-fun

∀[A,B:Type].
  ∀R:A ⟶ A ⟶ ℙ. ∀eq:EqDecider(B). ∀f:A ⟶ B. ∀L:A List.
    (l-ordered(A;x,y.R[x;y];L) ⇒ l-ordered(A;x,y.R[x;y];remove-repeats-fun(eq;f;L)))
BY
{ (InductionOnList
   THEN RepUR ``remove-repeats-fun`` 0
   THEN Try (Complete (Auto))
   THEN Try (Fold `remove-repeats-fun` 0)
   THEN (RW ListC 0 THEN Auto)
   THEN Try ((BLemma `l-ordered-filter` THEN Auto))
   THEN (RW ListC (-2) THENA Auto)
   THEN AllReduce
   THEN RepD
   THEN (RWO "remove-repeats-fun-member" (-3) THENA Auto)
   THEN ExRepD
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}eq:EqDecider(B).  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}L:A  List.
        (l-ordered(A;x,y.R[x;y];L)  {}\mRightarrow{}  l-ordered(A;x,y.R[x;y];remove-repeats-fun(eq;f;L)))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``remove-repeats-fun``  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Fold  `remove-repeats-fun`  0)
  THEN  (RW  ListC  0  THEN  Auto)
  THEN  Try  ((BLemma  `l-ordered-filter`  THEN  Auto))
  THEN  (RW  ListC  (-2)  THENA  Auto)
  THEN  AllReduce
  THEN  RepD
  THEN  (RWO  "remove-repeats-fun-member"  (-3)  THENA  Auto)
  THEN  ExRepD
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index