---

Step * of Lemma church-zero_wf2

No Annotations
cZ ∈ INat
BY
{ Unfold `indNat` 0 }

1
cZ ∈ x:cNat ⋂ church-inductive{i:l}(x)

---

Latex:

---

Latex:
No  Annotations
cZ  \mmember{}  INat


By

---

Latex:
Unfold  `indNat`  0

---

Home Index