---

Step * of Lemma isl-list-index

∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:T List.  (↑isl(list-index(eq;L;x)) ⇐⇒ (x ∈ L))
BY
{ (InductionOnList THEN Unfold `list-index` 0 THEN Reduce 0 THEN Try (Fold `list-index` 0)) }

1
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
⊢ False ⇐⇒ (x ∈ [])

2
1. [T] : Type
2. eq : EqDecider(T)
3. x : T
4. u : T
5. v : T List
6. ↑isl(list-index(eq;v;x)) ⇐⇒ (x ∈ v)
⊢ ↑isl(case list-index(eq;v;x)
   of inl(n) =>
   inl (n + 1)
   | inr(a) =>
   if eqof(eq) u x then inl 0 else list-index(eq;v;x) fi )
⇐⇒ (x ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}L:T  List.    (\muparrow{}isl(list-index(eq;L;x))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

---

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

---

Home Index