induction as with
| nil => rfl
| cons a as hi =>
  rw [cons_bind, map, cons_bind]
  rw [hi]
α : Type u
β : Type v
γ : Type w
f : α → β → γ
as : List α
bs : List β
⊢ (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
no goals