---

Step * 1 of Lemma bool-size_wf


1. k : ℤ
⊢ ∀[f:ℕ0 ⟶ 𝔹]. (0 ∈ ℕ1)
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
\mvdash{}  \mforall{}[f:\mBbbN{}0  {}\mrightarrow{}  \mBbbB{}].  (0  \mmember{}  \mBbbN{}1)


By

---

Latex:
xxxAutoxxx

---

Home Index