---

Step * of Lemma l_index_wf

∀[T:Type]. ∀[dT:EqDecider(T)]. ∀[L:T List]. ∀[x:T].  index(L;x) ∈ ℕ||L|| supposing (x ∈ L)
BY
{ ((UnivCD THENA Auto) THEN Unfold `l_index` 0 THEN BLemma `mu-bound` THEN Reduce 0 THEN Auto') }

1
1. T : Type
2. dT : EqDecider(T)
3. L : T List
4. x : T
5. (x ∈ L)
⊢ ∃n:ℕ||L||. (↑(dT x L[n]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[dT:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[x:T].    index(L;x)  \mmember{}  \mBbbN{}||L||  supposing  (x  \mmember{}  L)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `l\_index`  0  THEN  BLemma  `mu-bound`  THEN  Reduce  0  THEN  Auto')

---

Home Index