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
  H : ByteCompare.compare b b0 = Lt
  b1 : Byte.byte
  z : string
  H0 : ByteCompareSpec.lt b0 b1
  X : ByteCompare.compare b b1 = Lt
  ============================
   (Lt = Lt -> Lt = Lt -> Lt = Lt)


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