---

Step * of Lemma list-index_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:T List].  (list-index(eq;L;x) ∈ ℕ||L|| + Top)
BY
{ (InductionOnList THEN Unfold `list-index` 0 THEN Reduce 0 THEN Try (Fold `list-index` 0) THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[L:T  List].    (list-index(eq;L;x)  \mmember{}  \mBbbN{}||L||  +  Top)


By

---

Latex:
(InductionOnList  THEN  Unfold  `list-index`  0  THEN  Reduce  0  THEN  Try  (Fold  `list-index`  0)  THEN  Auto')

---

Home Index