---

Step * 1 2 1 1 1 of Lemma listify_wf

.....assertion..... 
1. T : Type
2. n : ℤ
3. m : {...n}
4. f : {m..n-} ⟶ T
⊢ ∀k:ℕ. ∀n:ℤ. ∀m:{...n}.  (n - m < k ⇒ (∀f:{m..n-} ⟶ T. (listify(f;m;n) ∈ T List)))
BY
{ (D 0 THENA Auto) }

1
1. T : Type
2. n : ℤ
3. m : {...n}
4. f : {m..n-} ⟶ T
5. k : ℕ
⊢ ∀n:ℤ. ∀m:{...n}.  (n - m < k ⇒ (∀f:{m..n-} ⟶ T. (listify(f;m;n) ∈ T List)))

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  m  :  \{...n\}
4.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
\mvdash{}  \mforall{}k:\mBbbN{}.  \mforall{}n:\mBbbZ{}.  \mforall{}m:\{...n\}.    (n  -  m  <  k  {}\mRightarrow{}  (\mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.  (listify(f;m;n)  \mmember{}  T  List)))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index