---

Step * 1 1 2 1 of Lemma listify_select_id

.....truecase..... 
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. n ≤ j
⊢ [] = [u / v] ∈ (T List)
BY
{ Auto' }

---

Latex:

---

Latex:
.....truecase..... 
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.  n  \mleq{}  j
\mvdash{}  []  =  [u  /  v]


By

---

Latex:
Auto'

---

Home Index