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


DEBUG:Going to execute:
simpl