---

Step * 1 of Lemma church-zero_wf2


cZ ∈ x:cNat ⋂ church-inductive{i:l}(x)
BY
{ (Unfold `member` 0 THEN DepIsectCD THEN Fold `member` 0) }

1
cZ ∈ cNat

2
cZ ∈ church-inductive{i:l}(cZ)

---

Latex:

---

Latex:

cZ  \mmember{}  x:cNat  \mcap{}  church-inductive\{i:l\}(x)


By

---

Latex:
(Unfold  `member`  0  THEN  DepIsectCD  THEN  Fold  `member`  0)

---

Home Index