---

Step * 1 1 1 1 of Lemma select_firstn


1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (∀i:ℕn - 1. (firstn(n - 1;as)[i] = as[i] ∈ T)))
5. 0 < n
6. u : T
7. v : T List
8. n ≤ (||v|| + 1)
9. i : ℕn
⊢ [u / firstn(n - 1;v)][i] = [u / v][i] ∈ T
BY
{ (Decide ⌜i = 0 ∈ ℤ⌝ THENA Auto) }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (∀i:ℕn - 1. (firstn(n - 1;as)[i] = as[i] ∈ T)))
5. 0 < n
6. u : T
7. v : T List
8. n ≤ (||v|| + 1)
9. i : ℕn
10. i = 0 ∈ ℤ
⊢ [u / firstn(n - 1;v)][i] = [u / v][i] ∈ T

2
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (∀i:ℕn - 1. (firstn(n - 1;as)[i] = as[i] ∈ T)))
5. 0 < n
6. u : T
7. v : T List
8. n ≤ (||v|| + 1)
9. i : ℕn
10. ¬(i = 0 ∈ ℤ)
⊢ [u / firstn(n - 1;v)][i] = [u / v][i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}as:T  List.  (((n  -  1)  \mleq{}  ||as||)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  (firstn(n  -  1;as)[i]  =  as[i])))
5.  0  <  n
6.  u  :  T
7.  v  :  T  List
8.  n  \mleq{}  (||v||  +  1)
9.  i  :  \mBbbN{}n
\mvdash{}  [u  /  firstn(n  -  1;v)][i]  =  [u  /  v][i]


By

---

Latex:
(Decide  \mkleeneopen{}i  =  0\mkleeneclose{}  THENA  Auto)

---

Home Index