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