---

Step * 1 1 of Lemma church-succ_wf2


1. x : x:cNat ⋂ church-inductive{i:l}(x)
2. x ∈ cNat
3. x ∈ church-inductive{i:l}(x)
⊢ cS x ∈ cNat
BY
{ Auto }

---

Latex:

---

Latex:

1.  x  :  x:cNat  \mcap{}  church-inductive\{i:l\}(x)
2.  x  \mmember{}  cNat
3.  x  \mmember{}  church-inductive\{i:l\}(x)
\mvdash{}  cS  x  \mmember{}  cNat


By

---

Latex:
Auto

---

Home Index