---

Step * of Lemma append_segment

∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}. ∀k:{j...||as||}.
  (((as[i..j-]) @ (as[j..k-])) = (as[i..k-]) ∈ (T List))
BY
{ (RepD THENA Auto) }

1
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
5. k : {j...||as||}
⊢ ((as[i..j-]) @ (as[j..k-])) = (as[i..k-]) ∈ (T List)

---

Latex:

---

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


By

---

Latex:
(RepD  THENA  Auto)

---

Home Index