proposition: Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) : x ∈ (guard P;; X) ↔ P ∧ x ∈ X.
proof: Proof. case_guard; rewrite elem_of_bind; [setoid_rewrite elem_of_ret | setoid_rewrite elem_of_mfail]; naive_solver. Qed.
imports: stdpp(finite) stdpp(options)