---

Step * 1 of Lemma listify_select_id


1. T : Type
2. as : T List
⊢ (λi:ℕ||as||. as[i])[ℕ||as||] = as ∈ (T List)
BY
{ (% Generalize Concl for induction %
   Assert ⌜∀n,j:ℕ.  (((j + ||as||) = n ∈ ℤ) ⇒ (listify(λi.as[i - j];j;n) = as ∈ (T List)))⌝
   THENA UnivCD
   THENA Auto) }

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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
\mvdash{}  (\mlambda{}i:\mBbbN{}||as||.  as[i])[\mBbbN{}||as||]  =  as


By

---

Latex:
(\%  Generalize  Concl  for  induction  \%
  Assert  \mkleeneopen{}\mforall{}n,j:\mBbbN{}.    (((j  +  ||as||)  =  n)  {}\mRightarrow{}  (listify(\mlambda{}i.as[i  -  j];j;n)  =  as))\mkleeneclose{}
  THENA  UnivCD
  THENA  Auto)

---

Home Index