---

Step * 1 1 of Lemma member-listify


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)
BY
{ xxx(Assert ⌜False⌝⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  m  :  \mBbbZ{}
3.  n  :  \{m..m  +  0\msupminus{}\}
4.  f  :  \{m..n\msupminus{}\}  {}\mrightarrow{}  T
5.  x  :  T
\mvdash{}  (x  \mmember{}  listify(f;m;n))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\{m..n\msupminus{}\}.  (x  =  (f  i))


By

---

Latex:
xxx(Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index