Goal:
  
  A : Type
  B : Type
  x : A
  x' : A
  y : B
  y' : B
  H : (x, y) = (x', y')
  H1 : x = x'
  H2 : y = y'
  ============================
   (x' = x')


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>