Goal:
    n : t
  ============================
   (n - n = match n with
            | Some _ => Some 0
            | None => None
            end)


DEBUG:Going to execute:
destruct n

Goals:
    z : Z
  ============================
   (Some z - Some z = Some 0)

  
  ============================
   (None - None = None)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: n