---

Step * 1 2 of Lemma select_l_index


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
BY
{ ((RWO "deq_property<" (-2)) THEN Try (Fold `l_index` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  dT  :  EqDecider(T)
3.  L  :  T  List
4.  x  :  T
5.  (x  \mmember{}  L)
6.  \muparrow{}(dT  x  L[mu(\mlambda{}i.(dT  x  L[i]))])
7.  \mforall{}[i:\mBbbN{}||L||].  \mneg{}\muparrow{}(dT  x  L[i])  supposing  i  <  mu(\mlambda{}i.(dT  x  L[i]))
\mvdash{}  L[mu(\mlambda{}i.(dT  x  L[i]))]  =  x


By

---

Latex:
((RWO  "deq\_property<"  (-2))  THEN  Try  (Fold  `l\_index`  0)  THEN  Auto)

---

Home Index