no goals
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : IsLawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → F β
h : β → G γ
f : β → γ
x✝ : t β
η : ApplicativeTransformation F G
x : t (F α)
⊢ (fun {α} => ApplicativeTransformation.app η α) (sequence x) =
    sequence ((fun {α} => ApplicativeTransformation.app η α) <$> x)
simp [sequence, naturality, traverse_map]