---

Step * 1 of Lemma append-segment


1. T : Type
2. i : {0...||[]||}
3. j : {i...||[]||}
4. k : {j...||[]||}
⊢ (firstn(j - i;nth_tl(i;[])) @ firstn(k - j;nth_tl(j;[]))) = firstn(k - i;nth_tl(i;[])) ∈ (T List)
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  i  :  \{0...||[]||\}
3.  j  :  \{i...||[]||\}
4.  k  :  \{j...||[]||\}
\mvdash{}  (firstn(j  -  i;nth\_tl(i;[]))  @  firstn(k  -  j;nth\_tl(j;[])))  =  firstn(k  -  i;nth\_tl(i;[]))


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index