---

Step * 1 of Lemma firstn_all


1. u : Top
2. v : Top List
3. ∀[n:ℤ]. firstn(n;v) ~ v supposing ||v|| ≤ n
4. n : ℤ
5. ¬0 < n
6. (||v|| + 1) ≤ n
⊢ [] ~ [u / v]
BY
{ Auto' }

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[n:\mBbbZ{}].  firstn(n;v)  \msim{}  v  supposing  ||v||  \mleq{}  n
4.  n  :  \mBbbZ{}
5.  \mneg{}0  <  n
6.  (||v||  +  1)  \mleq{}  n
\mvdash{}  []  \msim{}  [u  /  v]


By

---

Latex:
Auto'

---

Home Index