---

Step * 1 of Lemma hd_l_interval

.....equality..... 
1. T : Type
2. l : T List
3. i : ℕ||l||
4. j : ℕi
⊢ hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]
BY
{ RWO "select0" 0
THEN Auto }

---

Latex:

---

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


By

---

Latex:
RWO  "select0"  0
THEN  Auto

---

Home Index