---

Step * 2 1 of Lemma select-firstn


1. L : Top List
⊢ ∀m:ℕ||L||. ∀x:ℕm.  (firstn(m;L)[x] ~ L[x])
BY
{ xxx(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))xxx }

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:
xxx(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))xxx

---

Home Index