= a
     : nat
     = n + 0
     : nat