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 : x = y
  ============================
   (String b0 x = String b0 y)


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1