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