---

Step * 1 1 of Lemma firstn_length


1. u : Top
2. v : Top List
3. firstn(||v||;v) ~ v
4. 0 < ||v|| + 1
⊢ firstn((||v|| + 1) - 1;v) ~ v
BY
{ ((NthHypSq (-2)) THEN EqCD THEN EqCD THEN Auto') }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  firstn(||v||;v)  \msim{}  v
4.  0  <  ||v||  +  1
\mvdash{}  firstn((||v||  +  1)  -  1;v)  \msim{}  v


By

---

Latex:
((NthHypSq  (-2))  THEN  EqCD  THEN  EqCD  THEN  Auto')

---

Home Index