---

Step * 1 2 of Lemma select_listify_id


1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. i : ℕn
5. ∀j:{...n}. ((0 ≤ j) ⇒ (∀i:{j..n-}. (listify(f;j;n)[i - j] = (f i) ∈ T)))
⊢ (f)[ℕn][i] = (f i) ∈ T
BY
{ ((InstHyp [⌜0⌝;⌜i⌝] 5 THENM RW IntNormC (-1)) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  i  :  \mBbbN{}n
5.  \mforall{}j:\{...n\}.  ((0  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}i:\{j..n\msupminus{}\}.  (listify(f;j;n)[i  -  j]  =  (f  i))))
\mvdash{}  (f)[\mBbbN{}n][i]  =  (f  i)


By

---

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

---

Home Index