---

Step * 1 1 of Lemma listify_select_id


1. T : Type
2. as : T List
3. n : ℕ
4. j : ℕ
5. (j + ||as||) = n ∈ ℤ
⊢ listify(λi.as[i - j];j;n) = as ∈ (T List)
BY
{ (((MoveToConcl 4 THEN ListInd 2) THEN AbReduce 0) THEN (UnivCD THENA Auto)) }

1
1. T : Type
2. n : ℕ
3. j : ℕ
4. (j + 0) = n ∈ ℤ
⊢ listify(λi.⊥;j;n) = [] ∈ (T List)

2
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 ∈ ℤ
⊢ listify(λi.[u / v][i - j];j;n) = [u / v] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  n  :  \mBbbN{}
4.  j  :  \mBbbN{}
5.  (j  +  ||as||)  =  n
\mvdash{}  listify(\mlambda{}i.as[i  -  j];j;n)  =  as


By

---

Latex:
(((MoveToConcl  4  THEN  ListInd  2)  THEN  AbReduce  0)  THEN  (UnivCD  THENA  Auto))

---

Home Index