Goal:
    x : byte  y : byte
  ============================
   (reflectProp (x = y) match compare x y with
                        | Eq => true
                        | _ => false
                        end)


DEBUG:Going to execute:
destruct (compare_spec x y); constructor
DEBUG LTAC Evaluated term: eqb_compare
DEBUG LTAC Evaluated term: eqb_compare