no goals
F : Type u → Type w
G : Type v → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type v
f : α → β
x : Comp F G α
⊢ run (Seq.seq (pure f) fun x_1 => x) = run (f <$> x)
simp [Applicative.pure_seq_eq_map', functor_norm]