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


DEBUG:Going to execute:
destruct (ByteCompare.compare b0 b)

Goals:
  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> compare y z = Lt -> compare x z = Lt)

  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> Lt = Lt -> Lt = Lt)

  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> Gt = Lt -> Gt = Lt)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: (ByteCompare.compare b0 b)

Goals:
  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> compare y z = Lt -> compare x z = Lt)

  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> Lt = Lt -> Lt = Lt)

  
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  b : Byte.byte
  z : string
  ============================
   (compare x y = Lt -> Gt = Lt -> Gt = Lt)


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