---

Step * 2 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] ~ nth_tl(n;[u / v])
BY
{ (RecUnfold `nth_tl` 0 THEN SplitOnConclITE THEN Auto) }

---

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.  \mneg{}0  <  n
\mvdash{}  [u  /  v]  \msim{}  nth\_tl(n;[u  /  v])


By

---

Latex:
(RecUnfold  `nth\_tl`  0  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index