---

Step * of Lemma segment_factor

∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}.  ((as[i..j-]) = (Π i ≤ k < j. [as[k]]) ∈ (T List))
BY
{ ((RepD THENM Unfold `segment` 0) THENA Auto) }

1
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
⊢ firstn(j - i;nth_tl(i;as)) = (Π i ≤ k < j. [as[k]]) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.  \mforall{}i:\{0...||as||\}.  \mforall{}j:\{i...||as||\}.    ((as[i..j\msupminus{}])  =  (\mPi{}  i  \mleq{}  k  <  j.  [as[k]]))


By

---

Latex:
((RepD  THENM  Unfold  `segment`  0)  THENA  Auto)

---

Home Index