Prove traverse_compose for Lists without Axiom (Traversable.v)

[rudynicolop]

In ListTraversableSpec, the proof of traverse_compose

Lemma traverse_compose :
    forall {Q R : Type -> Type} `{QA : Applicative Q} `{RA : Applicative R}
      {A B C : Type} (f : A -> Q B) (h : B -> R C),
      @traverse (Q ∘ R) _ _ _ (@fmap Q _ B (R C) h ∘ f) =
      @fmap Q _ (list B) (R (list C)) (@traverse R _ B C h) ∘ (@traverse Q _ A B f).

uses the axiom:

Axiom switch_fun_args_app :
    forall {F : Type -> Type} `{Applicative F}
      {A B C : Type} (f : A -> B -> C) (a : F A) (b : F B),
      (fun x y => f x y) <$> a <*> b = (fun y x => f x y) <$> b <*> a.

I believe it to be true but I have as of yet been unable to formally verify it.