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


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>