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


DEBUG:Going to execute:
destruct (compare_spec s s')
DEBUG LTAC Evaluated term: eqb_compare
DEBUG LTAC Evaluated term: eqb_compare
DEBUG LTAC Evaluated term: (compare s s')