Goal:
  
  b : Byte.byte
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  ============================
   (lt "" (String b x))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>