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


DEBUG:Going to execute:
destruct d