Goal:
    z : Z  z0 : Z
  ============================
   (Some z + (Some z0 + None) = Some z + Some z0 + None)


DEBUG:Going to execute:
reflexivity
Level 1: Backtrace:

In environment
z, z0, z1 : Z
Unable to unify "Some z + Some z0 + Some z1" with
 "Some z + (Some z0 + Some z1)".
Level 0: Backtrace:

In environment
z, z0, z1 : Z
Unable to unify "Some z + Some z0 + Some z1" with
 "Some z + (Some z0 + Some z1)".