---

Step * 1 of Lemma finite-nat-seq-to-list-prop1


1. n : ℤ
2. f1 : ℕ0 ⟶ ℕ
⊢ (0 = 0 ∈ ℕ) ∧ (∀i:ℕ0. (⊥ = (f1 i) ∈ ℕ))
BY
{ Auto }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  f1  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  (0  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}0.  (\mbot{}  =  (f1  i)))


By

---

Latex:
Auto

---

Home Index