no goals
α✝ β✝ γ✝ : Type u
m✝ : ?m.20189
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x => b) = (fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b
simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map] <;> rfl