∀ {t : Type u → Type u} [inst : Traversable t] [toLawfulFunctor : LawfulFunctor t],
  (∀ {α : Type u} (x : t α), traverse pure x = pure x) →
    (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
        [LawfulApplicative G] {α β γ : Type u} (f : β → F γ) (g : α → G β) (x : t α),
        traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)) →
      (∀ {α β : Type u} (f : α → β) (x : t α), traverse (pure ∘ f) x = pure (f <$> x)) →
        (∀ {F G : Type u → Type u} [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F]
            [LawfulApplicative G] (η : ApplicativeTransformation F G) {α β : Type u} (f : α → F β) (x : t α),
            (fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x) →
          LawfulTraversable t