∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G] {α : Type u_1}
  {β γ : Type u} (f : β → F γ) (g : α → G β) (x : Option α),
  Option.traverse (Functor.Comp.mk ∘ (fun x => f <$> x) ∘ g) x =
    Functor.Comp.mk (Option.traverse f <$> Option.traverse g x)