---

Step * 1 2 1 of Lemma listify_select_id


1. T : Type
2. as : T List
3. ∀n,j:ℕ.  (((j + ||as||) = n ∈ ℤ) ⇒ (listify(λi.as[i - j];j;n) = as ∈ (T List)))
4. (λi.as[i - 0])[ℕ||as||] = as ∈ (T List)
⊢ (λi:ℕ||as||. as[i])[ℕ||as||] = as ∈ (T List)
BY
{ (NthHypEq (-1) THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

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


By

---

Latex:
(NthHypEq  (-1)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index