---

Step * 1 2 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)))
⊢ (λi:ℕ||as||. as[i])[ℕ||as||] = as ∈ (T List)
BY
{ ((InstHyp [⌜||as||⌝;⌜0⌝] 3 THENM RW IntNormC (-1)) THEN Auto') }

1
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)

---

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))
\mvdash{}  (\mlambda{}i:\mBbbN{}||as||.  as[i])[\mBbbN{}||as||]  =  as


By

---

Latex:
((InstHyp  [\mkleeneopen{}||as||\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  3  THENM  RW  IntNormC  (-1))  THEN  Auto')

---

Home Index