Goal:
  
  s : t
  s' : t
  e : match compare s s' with
      | Eq => true
      | _ => false
      end = false
  ============================
   (s <> s')


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrtclintros@0> arg
DEBUG LTAC Evaluated term: eqb_compare
DEBUG LTAC Evaluated term: eqb_compare
DEBUG LTAC Evaluated term: (compare s s')