Goal:
    A : Type  B : Type  C : Type  f : B -> C  p : A × B
  ============================
   ((on_snd f p).2 = f p.2)


DEBUG:Going to execute:
PTRDEBUGTACdestruct p