---

Step * of Lemma list-index-cmp_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[A:Type]. ∀[f:A ⟶ T].
  (list-index-cmp(eq;L;f) ∈ comparison({x:A| (f x ∈ L)} ))
BY
{ (ProveWfLemma THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].
    (list-index-cmp(eq;L;f)  \mmember{}  comparison(\{x:A|  (f  x  \mmember{}  L)\}  ))


By

---

Latex:
(ProveWfLemma  THEN  EAuto  1)

---

Home Index