---

Step * 1 of Lemma member-listify

.....assertion..... 
1. [T] : Type
⊢ ∀d:ℕ. ∀m:ℤ. ∀n:{m..m + d-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
BY
{ xxx(InductionOnNat THEN (UnivCD THENA Auto))xxx }

1
1. [T] : Type
2. m : ℤ
3. n : {m..m + 0-}
4. f : {m..n-} ⟶ T
5. x : T
⊢ (x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T)

2
1. [T] : Type
2. d : ℤ
3. [%1] : 0 < d
4. ∀m:ℤ. ∀n:{m..m + (d - 1)-}. ∀f:{m..n-} ⟶ T. ∀x:T.  ((x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T))
5. m : ℤ
6. n : {m..m + d-}
7. f : {m..n-} ⟶ T
8. x : T
⊢ (x ∈ listify(f;m;n)) ⇐⇒ ∃i:{m..n-}. (x = (f i) ∈ T)

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
\mvdash{}  \mforall{}d:\mBbbN{}.  \mforall{}m:\mBbbZ{}.  \mforall{}n:\{m..m  +  d\msupminus{}\}.  \mforall{}f:\{m..n\msupminus{}\}  {}\mrightarrow{}  T.  \mforall{}x:T.
        ((x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i)))


By

---

Latex:
xxx(InductionOnNat  THEN  (UnivCD  THENA  Auto))xxx

---

Home Index