---

Step * of Lemma whole_segment

∀T:Type. ∀as:T List.  ((as[0..||as||-]) = as ∈ (T List))
BY
{ ((Unfold `segment` 0 THEN Auto) THEN Reduce 0 THEN Subst' ||as|| - 0 ~ ||as|| 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `segment`  0  THEN  Auto)  THEN  Reduce  0  THEN  Subst'  ||as||  -  0  \msim{}  ||as||  0  THEN  Auto)

---

Home Index