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


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