proposition: Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P;; X) ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
proof: Proof. rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard. destruct (decide P); naive_solver. Qed.
imports: stdpp(finite) stdpp(options)