Goal:
    n : t
  ============================
   (n + Some 0 = n)


DEBUG:Going to execute:
destruct n; try reflexivity