Step
*
of Lemma
remove-repeats-fun_wf
∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[L:A List].  (remove-repeats-fun(eq;f;L) ∈ A List)
BY
{ ProveWfLemma }
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)  \mmember{}  A  List)
By
Latex:
ProveWfLemma
Home
Index