Update comment

stdpp/option.v

@@ -388,10 +388,9 @@ Section union_intersection_difference.
   Proof. apply union_with_proper. by constructor. Qed.
 End union_intersection_difference.
 
-(**
-  This lemma includes a bind, to avoid equalities of proofs.
-  A direct proof that `guard P = Some p` would require `decide P = left p`.
-*)
+(** This lemma includes a bind, to avoid equalities of proofs. We cannot have
+[guard P = Some p ↔ P] unless [P] is proof irrelant. The best (but less usable)
+self-contained alternative would be [guard P = Some p ↔ decide P = left p]. *)
 Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
   P → (guard P;; mx) = mx.
 Proof. intros. by case_guard. Qed.

stdpp/sets.v

@@ -946,10 +946,9 @@ Global Instance set_mfail `{MonadSet M} : MFail M := λ _, ∅.
 Section set_monad_base.
   Context `{MonadSet M}.
 
-  (**
-    This lemma includes a bind, to avoid equalities of proofs.
-    A direct proof that `p ∈ guard P` would require `decide P = left p`.
-  *)
+  (** This lemma includes a bind, to avoid equalities of proofs. We cannot have
+  [p ∈ guard P ↔ P] unless [P] is proof irrelant. The best (but less usable)
+  self-contained alternative would be [p ∈ guard P ↔ decide P = left p]. *)
   Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
     x ∈ (guard P;; X) ↔ P ∧ x ∈ X.
   Proof.