---

Step * 2 1 of Lemma select-firstn


1. L : Top List
⊢ ∀m:ℕ||L||. ∀x:ℕm.  (firstn(m;L)[x] ~ L[x])
BY
{ (ListInd 1
   THEN RecUnfold `firstn` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (UnivCD THENA Auto)
   THEN AutoSplit
   THEN CaseNat 0 `x'
   THEN Reduce 0
   THEN Try (Trivial)) }

1
1. u : Top
2. v : Top List
3. ∀m:ℕ||v||. ∀x:ℕm.  (firstn(m;v)[x] ~ v[x])
4. m : ℕ||v|| + 1
5. x : ℕm
6. 0 < m
7. ¬(x = 0 ∈ ℤ)
⊢ [u / firstn(m - 1;v)][x] ~ [u / v][x]

---

Latex:

---

Latex:

1.  L  :  Top  List
\mvdash{}  \mforall{}m:\mBbbN{}||L||.  \mforall{}x:\mBbbN{}m.    (firstn(m;L)[x]  \msim{}  L[x])


By

---

Latex:
(ListInd  1
  THEN  RecUnfold  `firstn`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (UnivCD  THENA  Auto)
  THEN  AutoSplit
  THEN  CaseNat  0  `x'
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index