Chaining two partial operations gives the same results in either bracketing when the operations agree pointwise.
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ζ : Type u_5} {ε : Type u_6} {f : α → β → Option γ} {g : γ → δ → Option ε} {f' : β → δ → Option ζ} {g' : α → ζ → Option ε} (h : ∀ (a : α) (b : β) (d : δ), ((f a b).bind fun (x : γ) => g x d) = (f' b d).bind fun (x : ζ) => g' a x) {s : α → Prop} {t : β → Prop} {u : δ → Prop} {e : ε} :
(∃ (c : γ), (∃ (a : α), s a ∧ ∃ (b : β), t b ∧ f a b = some c) ∧ ∃ (d : δ), u d ∧ g c d = some e) ↔ ∃ (a : α), s a ∧ ∃ (z : ζ), (∃ (b : β), t b ∧ ∃ (d : δ), u d ∧ f' b d = some z) ∧ g' a z = some e