Goal:
    A : Type  B : Type  C : Type  f : B -> C  a : A  b : B
  ============================
   ((on_snd f (a, b)).2 = f (a, b).2)


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: p