---

Step * of Lemma int-list-index_wf

∀[x:ℤ]. ∀[L:ℤ List].  (int-list-index(L;x) ∈ ℕ||L|| + 1)
BY
{ xxx(InductionOnList THEN Unfold `int-list-index` 0 THEN Reduce 0 THEN Try (Fold `int-list-index` 0) THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[L:\mBbbZ{}  List].    (int-list-index(L;x)  \mmember{}  \mBbbN{}||L||  +  1)


By

---

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

---

Home Index