Theorem: Option.forall_mem_bind (HMem/Trace/Sound.lean)

State before:
α : Type u_1
β : Type u_2
f : α → Option β
o : Option α
p : β → Prop
⊢ (∀ y ∈ Option.bind o f, p y) ↔ ∀ x ∈ o, ∀ y ∈ f x, p y
Tactic:
simpa using ⟨ λ h _ hx _ ↦ h _ _ hx, λ h _ _ hx ↦ h _ hx _ ⟩
State after:
no goals