Goal:
    A : Type  B : Type  C : Type  D : Type  f : C -> D  g : B -> C
  ============================
   ((fun x : A × B => on_snd f (on_snd g x)) = on_snd (fun x : B => f (g x)))


DEBUG:Going to execute:
reflexivity