---

Step * of Lemma hd_l_interval

∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi].  (hd(l_interval(l;j;i)) = l[j] ∈ T)
BY
{ ((UnivCD THENA Auto) THEN Subst ⌜hd(l_interval(l;j;i)) ~ l_interval(l;j;i)[0]⌝ 0⋅) }

1
.....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]

2
1. T : Type
2. l : T List
3. i : ℕ||l||
4. j : ℕi
⊢ l_interval(l;j;i)[0] = l[j] ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[i:\mBbbN{}||l||].  \mforall{}[j:\mBbbN{}i].    (hd(l\_interval(l;j;i))  =  l[j])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Subst  \mkleeneopen{}hd(l\_interval(l;j;i))  \msim{}  l\_interval(l;j;i)[0]\mkleeneclose{}  0\mcdot{})

---

Home Index