Goal:
  
  ============================
   (forall x y : string, CompareSpec (x = y) (lt x y) (lt y x) (compare x y))


DEBUG:Going to execute:
induction x; destruct y
DEBUG LTAC Evaluated term: ByteCompareSpec.compare_opp
DEBUG LTAC Evaluated term: ByteCompareSpec.compare_opp
DEBUG LTAC Evaluated term: CompOpp_iff
DEBUG LTAC Evaluated term: pf