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


DEBUG:Going to execute:
destruct z
Level 0: Backtrace:

Tactic failure: congruence failed.
Level 0: Backtrace:

Tactic failure: congruence failed.

Goals:
    b : Byte.byte  y : string
  ============================
   (Lt = Lt -> Gt = Lt -> Eq = Lt)

    b : Byte.byte  y : string  b0 : Byte.byte  z : string
  ============================
   (Lt = Lt ->
    match ByteCompare.compare b b0 with
    | Eq => compare y z
    | Lt => Lt
    | Gt => Gt
    end = Lt -> Lt = Lt)


DEBUG:Going to execute:
congruence

Goals:
    b : Byte.byte  y : string
  ============================
   (Lt = Lt -> Gt = Lt -> Eq = Lt)

    b : Byte.byte  y : string  b0 : Byte.byte  z : string
  ============================
   (Lt = Lt ->
    match ByteCompare.compare b b0 with
    | Eq => compare y z
    | Lt => Lt
    | Gt => Gt
    end = Lt -> Lt = Lt)


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1