---

Step * 1 of Lemma append_firstn_lastn_sq


1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. 0 < n
⊢ [u / v] ~ [u / (firstn(n - 1;v) @ nth_tl(n;[u / v]))]
BY
{ (EqCD THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀[n:ℕ||v|| + 1]. (v ~ firstn(n;v) @ nth_tl(n;v))
4. n : ℕ||[u / v]|| + 1
5. 0 < n
⊢ v ~ firstn(n - 1;v) @ nth_tl(n;[u / v])

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbN{}||v||  +  1].  (v  \msim{}  firstn(n;v)  @  nth\_tl(n;v))
4.  n  :  \mBbbN{}||[u  /  v]||  +  1
5.  0  <  n
\mvdash{}  [u  /  v]  \msim{}  [u  /  (firstn(n  -  1;v)  @  nth\_tl(n;[u  /  v]))]


By

---

Latex:
(EqCD  THEN  Try  (Trivial))

---

Home Index