---

Step * 1 of Lemma select_l_index


1. T : Type
2. dT : EqDecider(T)
3. L : T List
4. x : T
5. (x ∈ L)
⊢ L[index(L;x)] = x ∈ T
BY
{ (Unfold `l_index` 0 THEN (InstLemma `mu-bound-property` [⌜||L||⌝; ⌜λi.(dT x L[i])⌝])⋅ THEN Auto' THEN All Reduce) }

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

2
1. T : Type
2. dT : EqDecider(T)
3. L : T List
4. x : T
5. (x ∈ L)
6. ↑(dT x L[mu(λi.(dT x L[i]))])
7. ∀[i:ℕ||L||]. ¬↑(dT x L[i]) supposing i < mu(λi.(dT x L[i]))
⊢ L[mu(λi.(dT x L[i]))] = x ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  dT  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  (x  \mmember{}  L)
\mvdash{}  L[index(L;x)]  =  x


By

---

Latex:
(Unfold  `l\_index`  0
  THEN  (InstLemma  `mu-bound-property`  [\mkleeneopen{}||L||\mkleeneclose{};  \mkleeneopen{}\mlambda{}i.(dT  x  L[i])\mkleeneclose{}])\mcdot{}
  THEN  Auto'
  THEN  All  Reduce)

---

Home Index