---

Step * 1 1 2 1 of Lemma select_listify_id

.....falsecase..... 
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. (0 ≤ (j + 1)) ⇒ (∀i:{j + 1..n-}. (listify(f;j + 1;n)[i - j + 1] = (f i) ∈ T))
6. 0 ≤ j
7. i : {j..n-}@i
8. j < n
⊢ [f j / listify(f;j + 1;n)][i - j] = (f i) ∈ T
BY
{ (Decide ⌜i = j ∈ ℤ⌝ THENA Auto) }

1
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. (0 ≤ (j + 1)) ⇒ (∀i:{j + 1..n-}. (listify(f;j + 1;n)[i - j + 1] = (f i) ∈ T))
6. 0 ≤ j
7. i : {j..n-}@i
8. j < n
9. i = j ∈ ℤ
⊢ [f j / listify(f;j + 1;n)][i - j] = (f i) ∈ T

2
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. (0 ≤ (j + 1)) ⇒ (∀i:{j + 1..n-}. (listify(f;j + 1;n)[i - j + 1] = (f i) ∈ T))
6. 0 ≤ j
7. i : {j..n-}@i
8. j < n
9. ¬(i = j ∈ ℤ)
⊢ [f j / listify(f;j + 1;n)][i - j] = (f i) ∈ T

---

Latex:

---

Latex:
.....falsecase..... 
1.  T  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  j  :  \{...n  -  1\}@i
5.  (0  \mleq{}  (j  +  1))  {}\mRightarrow{}  (\mforall{}i:\{j  +  1..n\msupminus{}\}.  (listify(f;j  +  1;n)[i  -  j  +  1]  =  (f  i)))
6.  0  \mleq{}  j
7.  i  :  \{j..n\msupminus{}\}@i
8.  j  <  n
\mvdash{}  [f  j  /  listify(f;j  +  1;n)][i  -  j]  =  (f  i)


By

---

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

---

Home Index