no goals
β : Type u_1
γ : Type u_2
α : Type u_3
f : β → γ
g : α → List β
a : α
l : List α
⊢ map f (List.bind (a :: l) g) = List.bind (a :: l) fun a => map f (g a)
simp only [cons_bind, map_append, bind_map _ _ l]