Goal:
  
  y1 : V.t
  x2 : V.t
  n2 : Z
  y2 : V.t
  H3 : CompareSpec (y1 = y2) (V.lt y1 y2) (V.lt y2 y1) (V.compare y1 y2)
  ============================
   (CompareSpec ((x2, n2, y1) = (x2, n2, y2))
      (V.lt x2 x2 \/
       V.eq x2 x2 /\ n2 < n2 \/ V.eq x2 x2 /\ n2 = n2 /\ V.lt y1 y2)
      (V.lt x2 x2 \/
       V.eq x2 x2 /\ n2 < n2 \/ V.eq x2 x2 /\ n2 = n2 /\ V.lt y2 y1)
      (V.compare y1 y2))


DEBUG:Going to execute:
destruct (V.compare y1 y2); cbn in *; inversion_clear H3;
            constructor; subst
DEBUG LTAC Evaluated term: (V.compare_spec y1 y2)