no goals
ι : Type ?u.2509
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
g : β → List γ
f : α → β
a : α
l : List α
⊢ List.bind (map f (a :: l)) g = List.bind (a :: l) fun a => g (f a)
simp only [cons_bind, map_cons, map_bind _ _ l]