no goals
ι : Type ?u.22576
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
l : List α
f : α → List β
g : β → List γ
⊢ List.bind (List.bind l f) g = List.bind l fun x => List.bind (f x) g
induction l <;> simp [*]