---

Step * 1 1 1 of Lemma select_listify_id


1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. 0 ≤ n
5. i : {n..n-}@i
⊢ listify(f;n;n)[i - n] = (f i) ∈ T
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Auto

---

Home Index