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


DEBUG:Going to execute:
intros [[x1 n1] y1] [[x2 n2] y2]