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


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

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

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