---

Step * 1 2 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 ∈ church-inductive{i:l}(cS x)
BY
{ (InstLemma `church-iS` [⌜x⌝]⋅ THEN 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{}  church-inductive\{i:l\}(cS  x)


By

---

Latex:
(InstLemma  `church-iS`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index