---

Step * 1 1 1 of Lemma listify_select_id


1. T : Type
2. n : ℕ
3. j : ℕ
4. (j + 0) = n ∈ ℤ
⊢ listify(λi.⊥;j;n) = [] ∈ (T List)
BY
{ (RecUnfold `listify` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  j  :  \mBbbN{}
4.  (j  +  0)  =  n
\mvdash{}  listify(\mlambda{}i.\mbot{};j;n)  =  []


By

---

Latex:
(RecUnfold  `listify`  0  THEN  Auto)

---

Home Index