---

Step * 1 of Lemma length_segment


1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
⊢ ||as[i..j-]|| = (j - i) ∈ ℤ
BY
{ (RWW "u:segment length_firstn length_nth_tl" 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  i  :  \{0...||as||\}
4.  j  :  \{i...||as||\}
\mvdash{}  ||as[i..j\msupminus{}]||  =  (j  -  i)


By

---

Latex:
(RWW  "u:segment  length\_firstn  length\_nth\_tl"  0  THEN  Auto')

---

Home Index