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


DEBUG:Going to execute:
inversion 1
DEBUG LTAC Evaluated term: andb_true_iff
DEBUG LTAC Evaluated term: andb_and