∀ {α : Type u_3} {β : Type u_4} {γ : Type u_2} {δ : Type u_1} {f : α → β → γ} {a : Option α} {b : Option β}
  {α' : Type u_5} {g : γ → δ} {f' : β → α' → δ} {g' : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' b (g' a)) → Option.map g (Option.map₂ f a b) = Option.map₂ f' b (Option.map g' a)