Goal:
    A : Type  B : Type  f : A -> B  g : A -> B  H : forall x : A, f x = g x
  ============================
   (forall z : option A, option_map f z = option_map g z)


DEBUG:Going to execute:
intros []; cbn