Goal:
    x : Z  y : Z
  ============================
   (ssrbool.reflect (x = y) (x =? y))


DEBUG:Going to execute:
apply Z.eqb_spec
DEBUG LTAC Evaluated term: reflect_reflectProp