---

Step * of Lemma whole_segment

∀T:Type. ∀as:T List.  ((as[0..||as||-]) = as ∈ (T List))
BY
{ ((RepD THENM RWO "segment_factor" 0) THENA Auto{2,3}-1') }

1
1. T : Type@i'
2. as : T List@i
⊢ (Π 0 ≤ k < ||as||. [as[k]]) = as ∈ (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.    ((as[0..||as||\msupminus{}])  =  as)


By

---

Latex:
((RepD  THENM  RWO  "segment\_factor"  0)  THENA  Auto\{2,3\}-1')

---

Home Index