∀[a:Atom2]. ∀[n:ℕ].  a#n:ℕ
{ InductionOnNat }
.....basecase..... 
1. a : Atom2
2. n : ℤ
⊢ a#0:ℕ
.....upcase..... 
1. a : Atom2
2. n : ℤ
3. 0 < n
4. a#n - 1:ℕ
⊢ a#n:ℕ