Goal:
    z1 : Z  z2 : Z
  ============================
   (Some (z1 + z2)%Z = Some z1 + Some z2)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>