---

Step * 1 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
⊢ v ~ firstn(n - 1;v) @ nth_tl(n;[u / v])
BY
{ ((InstHyp [⌜n - 1⌝] 3)⋅ THENA Auto') }

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
6. v ~ firstn(n - 1;v) @ nth_tl(n - 1;v)
⊢ 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{}  v  \msim{}  firstn(n  -  1;v)  @  nth\_tl(n;[u  /  v])


By

---

Latex:
((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  3)\mcdot{}  THENA  Auto')

---

Home Index