diff --git a/CHANGELOG.md b/CHANGELOG.md
index ebe3c7c355e84296b21d279e735f78b39b5f358f..cae816829a558c232b79add1e274acbd7e806d6d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,17 @@ API-breaking change is listed.
     longer work for multisets.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
+- Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
+- Add `option_guard_True_pi`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i -E '
+s/\bdecide_left\b/decide_True_pi/g
+s/\bdecide_right\b/decide_False_pi/g
+' $(find theories -name "*.v")
+```
 
 ## std++ 1.5.0
 
diff --git a/theories/decidable.v b/theories/decidable.v
index 310eff9a1803fce53454c1195323f7cf206b0680..89b74b2e74aec5081614b8d613007a5ffedc3d99 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -25,9 +25,9 @@ Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
 Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
-Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
+Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
 Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
-Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
+Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
 Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
 
 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
diff --git a/theories/option.v b/theories/option.v
index 13de994cee7ef9cc060e4084ea8b4d7a27b75a22..7c10bc438c4a1eaaa0c32921b30249edb215605c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -339,10 +339,14 @@ Tactic Notation "case_option_guard" :=
   let H := fresh in case_option_guard as H.
 
 Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
-  P → (guard P; mx) = mx.
+  P → mguard P (λ _, mx) = mx.
 Proof. intros. by case_option_guard. Qed.
-Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
-  ¬P → (guard P; mx) = None.
+Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A)
+    (HP : P) :
+  mguard P f = f HP.
+Proof. intros. case_option_guard; [|done]. f_equal; apply proof_irrel. Qed.
+Lemma option_guard_False {A} P `{Decision P} (f : P → option A) :
+  ¬P → mguard P f = None.
 Proof. intros. by case_option_guard. Qed.
 Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
   (P ↔ Q) → (guard P; mx) = guard Q; mx.