---

Step * 1 1 2 2 of Lemma listify_select_id


1. T : Type
2. n : ℕ
3. u : T
4. v : T List
5. ∀j:ℕ. (((j + ||v||) = n ∈ ℤ) ⇒ (listify(λi.v[i - j];j;n) = v ∈ (T List)))
6. j : ℕ
7. (j + ||v|| + 1) = n ∈ ℤ
8. j < n
⊢ [[u / v][j - j] / listify(λi.[u / v][i - j];j + 1;n)] = [u / v] ∈ (T List)
BY
{ (EqCD THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
2:n
1. T : Type
2. n : ℕ
3. u : T
4. v : T List
5. ∀j:ℕ. (((j + ||v||) = n ∈ ℤ) ⇒ (listify(λi.v[i - j];j;n) = v ∈ (T List)))
6. j : ℕ
7. (j + ||v|| + 1) = n ∈ ℤ
8. j < n
⊢ listify(λi.[u / v][i - j];j + 1;n) = v ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}j:\mBbbN{}.  (((j  +  ||v||)  =  n)  {}\mRightarrow{}  (listify(\mlambda{}i.v[i  -  j];j;n)  =  v))
6.  j  :  \mBbbN{}
7.  (j  +  ||v||  +  1)  =  n
8.  j  <  n
\mvdash{}  [[u  /  v][j  -  j]  /  listify(\mlambda{}i.[u  /  v][i  -  j];j  +  1;n)]  =  [u  /  v]


By

---

Latex:
(EqCD  THEN  Try  (Complete  (Auto)))

---

Home Index