---

Step * of Lemma remove-repeats-fun-sublist

∀[A,B:Type].  ∀eq:EqDecider(B). ∀f:A ⟶ B. ∀L:A List.  remove-repeats-fun(eq;f;L) ⊆ L
BY
{ (InductionOnList
   THEN RepUR ``remove-repeats-fun`` 0
   THEN Try (Complete (Auto))
   THEN Fold `remove-repeats-fun` 0
   THEN (BLemma `cons_sublist_cons` THENA Auto)
   THEN (OrLeft THEN Auto)
   THEN (InstLemma `filter_is_sublist` [⌜A⌝;⌜remove-repeats-fun(eq;f;v)⌝;⌜λx.(¬b(eq (f x) (f u)))⌝]⋅ THENA Auto)
   THEN FLemma `sublist_transitivity` [-1;-3]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}eq:EqDecider(B).  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}L:A  List.    remove-repeats-fun(eq;f;L)  \msubseteq{}  L


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``remove-repeats-fun``  0
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `remove-repeats-fun`  0
  THEN  (BLemma  `cons\_sublist\_cons`  THENA  Auto)
  THEN  (OrLeft  THEN  Auto)
  THEN  (InstLemma  `filter\_is\_sublist`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}remove-repeats-fun(eq;f;v)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  u)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  FLemma  `sublist\_transitivity`  [-1;-3]
  THEN  Auto)

---

Home Index