---

Step * 1 2 1 2 of Lemma listify_wf


1. T : Type
2. n : ℤ
3. ∀m:{...n}. ∀f:{m..n-} ⟶ T.  (listify(f;m;n) ∈ T List)
4. m : ℤ
5. f : {m..n-} ⟶ T
6. ¬(m > n)
⊢ listify(f;m;n) ∈ T List
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  \mforall{}m:\{...n\}.  \mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.    (listify(f;m;n)  \mmember{}  T  List)
4.  m  :  \mBbbZ{}
5.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
6.  \mneg{}(m  >  n)
\mvdash{}  listify(f;m;n)  \mmember{}  T  List


By

---

Latex:
TACTIC:Auto

---

Home Index