---

Step * 2 of Lemma hd_l_interval


1. T : Type
2. l : T List
3. i : ℕ||l||
4. j : ℕi
⊢ l_interval(l;j;i)[0] = l[j] ∈ T
BY
{ (RWO "select_l_interval" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  i  :  \mBbbN{}||l||
4.  j  :  \mBbbN{}i
\mvdash{}  l\_interval(l;j;i)[0]  =  l[j]


By

---

Latex:
(RWO  "select\_l\_interval"  0  THEN  Auto')

---

Home Index