---

Step * of Lemma church-succ_wf2

No Annotations
cS ∈ INat ⟶ INat
BY
{ ((FunExt THENA Auto) THEN All (Unfold `indNat`) THEN DepIsectHD 1) }

1
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)

---

Latex:

---

Latex:
No  Annotations
cS  \mmember{}  INat  {}\mrightarrow{}  INat


By

---

Latex:
((FunExt  THENA  Auto)  THEN  All  (Unfold  `indNat`)  THEN  DepIsectHD  1)

---

Home Index