---

Step * of Lemma whole_segment_example

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

1
1. T : Type
2. as : T List
⊢ (Π 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')

---

Home Index