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


DEBUG:Going to execute:
rewrite H