---

Step * 1 2 1 of Lemma listify_wf


1. T : Type
2. n : ℤ
⊢ ∀m:ℤ. ∀f:{m..n-} ⟶ T.  ((¬(m > n)) ⇒ (listify(f;m;n) ∈ T List))
BY
{ (Assert ⌜∀m:{...n}. ∀f:{m..n-} ⟶ T.  (listify(f;m;n) ∈ T List)⌝ THEN (RepD THENA Auto)) }

1
1. T : Type
2. n : ℤ
3. m : {...n}
4. f : {m..n-} ⟶ T
⊢ listify(f;m;n) ∈ T List

2
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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}m:\{...n\}.  \mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.    (listify(f;m;n)  \mmember{}  T  List)\mkleeneclose{}  THEN  (RepD  THENA  Auto))

---

Home Index