Step * of Lemma free-from-atom2-nat

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

1
.....basecase..... 
1. Atom2
2. : ℤ
⊢ a#0:ℕ

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


Latex:


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


By


Latex:
InductionOnNat




Home Index