---

Step * of Lemma free-from-atom-nat

∀[a:Atom1]. ∀[n:ℕ].  a#n:ℕ
BY
{ InductionOnNat }

1
.....basecase..... 
1. a : Atom1
2. n : ℤ
⊢ a#0:ℕ

2
.....upcase..... 
1. a : Atom1
2. n : ℤ
3. 0 < n
4. a#n - 1:ℕ
⊢ a#n:ℕ

---

Latex:

---

Latex:
\mforall{}[a:Atom1].  \mforall{}[n:\mBbbN{}].    a\#n:\mBbbN{}


By

---

Latex:
InductionOnNat

---

Home Index