no goals
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ (Seq.seq (f <$> x) fun x => g <$> y) = Seq.seq ((flip (fun x x_1 => x ∘ x_1) g ∘ f) <$> x) fun x => y
simp [flip, functor_norm]