---

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