---

Step * of Lemma mklist_member

∀[T:Type]. ∀n:ℕ. ∀f:ℕn ⟶ T. ∀x:T.  ((x ∈ mklist(n;f)) ⇐⇒ ∃i:ℕn. (x = (f i) ∈ T))
BY
{ Auto }

1
1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. x : T
5. (x ∈ mklist(n;f))
⊢ ∃i:ℕn. (x = (f i) ∈ T)

2
1. [T] : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. x : T
5. ∃i:ℕn. (x = (f i) ∈ T)
⊢ (x ∈ mklist(n;f))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  T.  \mforall{}x:T.    ((x  \mmember{}  mklist(n;f))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (x  =  (f  i)))


By

---

Latex:
Auto

---

Home Index