rw [cons_bind, map, cons_bind]
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
a : α
as : List α
hi : (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
⊢ (List.bind (a :: as) fun a => map (f a) bs) = List.bind (map f (a :: as)) fun f => map f bs
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
bs : List β
a : α
as : List α
hi : (List.bind as fun a => map (f a) bs) = List.bind (map f as) fun f => map f bs
⊢ (map (f a) bs ++ List.bind as fun a => map (f a) bs) = map (f a) bs ++ List.bind (map f as) fun f => map f bs