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


DEBUG:Going to execute:
destruct (IHx y)

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

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

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


DEBUG:Going to execute:
constructor
DEBUG LTAC Evaluated term: (IHx y)

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

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

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


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

Goals:
  
  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)

  
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  H : lt x y
  ============================
   (Lt = Lt)

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


DEBUG:Going to execute:
eauto

Goals:
  
  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)

  
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  H : lt x y
  ============================
   (Lt = Lt)

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


DEBUG:Going to execute:
<coq-core.plugins.ltac::eauto@0> $1 $2 $3