cases hg:g c <;> simp [flatMap, flip, Option.bind, hg]
θ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Zero θ
x : CostFunction α θ
f : β → Option α
g : γ → Option β
c : γ
⊢ flatMap (flip Option.bind f ∘ g) x c = flatMap g (flatMap f x) c
no goals