no goals
α : Type u_2
β : Type u_1
γ : Type ?u.4731
δ : Type ?u.4734
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → Option β
x : Option α
⊢ (pbind x fun a x => f a) = Option.bind x f
cases x <;> simp only [pbind, none_bind', some_bind']