∀ {t t' : Type u → Type u} (eqv : (α : Type u) → t α ≃ t' α) [inst : Traversable t] [LawfulTraversable t]
  {F G : Type u → Type u} [inst_2 : Applicative F] [inst_3 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t' α),
  Equiv.traverse eqv (Functor.Comp.mk ∘ Functor.map f ∘ g) x =
    Functor.Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)