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)
      (match ByteCompare.compare b b0 with
       | Eq => compare x y
       | Lt => Lt
       | Gt => Gt
       end = Lt)
      (match ByteCompare.compare b0 b with
       | Eq => compare y x
       | Lt => Lt
       | Gt => Gt
       end = Lt)
      match ByteCompare.compare b b0 with
      | Eq => compare x y
      | Lt => Lt
      | Gt => Gt
      end)


DEBUG:Going to execute:
destruct (ByteCompareSpec.compare_spec b b0)

Goals:
  
  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
  H : b = b0
  ============================
   (CompareSpec (String b x = String b0 y) (compare x y = Lt)
      (match ByteCompare.compare b0 b with
       | Eq => compare y x
       | Lt => Lt
       | Gt => Gt
       end = Lt) (compare x y))

  
  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
  H : ByteCompareSpec.lt b b0
  ============================
   (CompareSpec (String b x = String b0 y) (Lt = Lt)
      (match ByteCompare.compare b0 b with
       | Eq => compare y x
       | Lt => Lt
       | Gt => Gt
       end = Lt) Lt)

  
  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
  H : ByteCompareSpec.lt b0 b
  ============================
   (CompareSpec (String b x = String b0 y) (Gt = Lt)
      (match ByteCompare.compare b0 b with
       | Eq => compare y x
       | Lt => Lt
       | Gt => Gt
       end = Lt) Gt)


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: (ByteCompareSpec.compare_spec b b0)