---

Step * 2 of Lemma select-firstn


1. L : Top List
2. n : ℕ
3. x : ℕn
4. ¬(||L|| ≤ n)
⊢ firstn(n;L)[x] ~ L[x]
BY
{ (MoveToConcl (-2) THEN (GenConcl ⌜n = m ∈ ℕ||L||⌝⋅ THENA Auto) THEN ThinVar `n' THEN MoveToConcl (-1)) }

1
1. L : Top List
⊢ ∀m:ℕ||L||. ∀x:ℕm.  (firstn(m;L)[x] ~ L[x])

---

Latex:

---

Latex:

1.  L  :  Top  List
2.  n  :  \mBbbN{}
3.  x  :  \mBbbN{}n
4.  \mneg{}(||L||  \mleq{}  n)
\mvdash{}  firstn(n;L)[x]  \msim{}  L[x]


By

---

Latex:
(MoveToConcl  (-2)  THEN  (GenConcl  \mkleeneopen{}n  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `n'  THEN  MoveToConcl  (-1))

---

Home Index