Goal:
    A : Type  B : Type  x : A  x' : A  y : B  y' : B
  ============================
   ((x, y) = (x', y') -> y = y')


DEBUG:Going to execute:
inversion 1