---

Step * of Lemma nat-id-fun-example

∀n:ℕ. (∃m:ℕ [(m = n ∈ ℕ)])
BY
{ ((CompleteInductionOnNat THENA Auto) THEN CaseNat 0 `n') }

1
1. n : ℕ
2. ∀n:ℕn. (∃m:ℕ [(m = n ∈ ℕ)])
3. n = 0 ∈ ℤ
⊢ ∃m:ℕ [(m = 0 ∈ ℕ)]

2
1. n : ℕ
2. ∀n:ℕn. (∃m:ℕ [(m = n ∈ ℕ)])
3. ¬(n = 0 ∈ ℤ)
⊢ ∃m:ℕ [(m = n ∈ ℕ)]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\mBbbN{}  [(m  =  n)])


By

---

Latex:
((CompleteInductionOnNat  THENA  Auto)  THEN  CaseNat  0  `n')

---

Home Index