---

Step * 1 2 1 1 of Lemma listify_wf


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

1
.....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)))

2
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)))
⊢ listify(f;m;n) ∈ T List

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}

---

Home Index