Goal:
  
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  H : lt y x
  ============================
   (compare y x = Lt)


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| Ltac.reflexivity
| Ltac.symmetry; trivial
| contradiction ]