Goal:
    x1 : V.t  n1 : Z  y1 : V.t  x2 : V.t  n2 : Z  y2 : V.t
  ============================
   (CompareSpec ((x1, n1, y1) = (x2, n2, y2)) (lt (x1, n1, y1) (x2, n2, y2))
      (lt (x2, n2, y2) (x1, n1, y1)) (compare (x1, n1, y1) (x2, n2, y2)))


DEBUG:Going to execute:
cbn