---

Step * 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 ∈ x:cNat ⋂ church-inductive{i:l}(x)
BY
{ DepIsectCD }

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

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

---

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{}  x:cNat  \mcap{}  church-inductive\{i:l\}(x)


By

---

Latex:
DepIsectCD

---

Home Index