---

Step * of Lemma firstn_all

∀[L:Top List]. ∀[n:ℤ].  firstn(n;L) ~ L supposing ||L|| ≤ n
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN RecUnfold `firstn` 0 THEN Reduce 0 THEN Auto THEN AutoSplit) }

1
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]

---

Latex:

---

Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbZ{}].    firstn(n;L)  \msim{}  L  supposing  ||L||  \mleq{}  n


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index