rw [hi]
case cons
α β : Type u
γ : Type w
f : α → List β
g : β → List γ
a : α
as : List α
hi : List.bind (List.bind as f) g = List.bind as fun x => List.bind (f x) g
⊢ List.bind (f a) g ++ List.bind (List.bind as f) g = List.bind (f a) g ++ List.bind as fun x => List.bind (f x) g
no goals