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


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

Goals:
  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : b = b0
  ============================
   (forall z : t,
    compare x y = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)

  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : ByteCompareSpec.lt b b0
  ============================
   (forall z : t,
    Lt = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)

  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : ByteCompareSpec.lt b0 b
  ============================
   (forall z : t,
    Gt = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)


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

Goals:
  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : b = b0
  ============================
   (forall z : t,
    compare x y = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)

  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : ByteCompareSpec.lt b b0
  ============================
   (forall z : t,
    Lt = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)

  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  b0 : Byte.byte
  y : string
  H : ByteCompareSpec.lt b0 b
  ============================
   (forall z : t,
    Gt = Lt ->
    match z with
    | ""%bs => Gt
    | String y0 ys =>
        match ByteCompare.compare b0 y0 with
        | Eq => compare y ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt ->
    match z with
    | ""%bs => Gt
    | String y ys =>
        match ByteCompare.compare b y with
        | Eq => compare x ys
        | Lt => Lt
        | Gt => Gt
        end
    end = Lt)


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>