no goals
F : Type u → Type v
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
G : Type u → Type w
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
x : α → β
y : F α
⊢ (fun {α} => app η α) (x <$> y) = x <$> (fun {α} => app η α) y
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]