---

Step * 2 1 of Lemma firstn_append


1. u : Top
2. v : Top List
3. ∀[L2:Top List]. ∀[n:ℕ||v|| + 1].  (firstn(n;v @ L2) ~ firstn(n;v))
4. L2 : Top List
5. n : ℕ(||v|| + 1) + 1
6. 0 < n
⊢ firstn(n - 1;v @ L2) ~ firstn(n - 1;v)
BY
{ (BackThruSomeHyp THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
(BackThruSomeHyp  THEN  Auto')

---

Home Index