Goal:
  
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  H : lt y x
  ============================
   (match ByteCompare.compare b0 b0 with
    | Eq => compare y x
    | Lt => Lt
    | Gt => Gt
    end = Lt)


DEBUG:Going to execute:
rewrite ByteCompareSpec.compare_eq_refl