diff --git a/theories/option.v b/theories/option.v
index 6a458aa459f33e99c164fdc0d86b0e5412ce206c..7c10bc438c4a1eaaa0c32921b30249edb215605c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -339,7 +339,7 @@ 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_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A)
     (HP : P) :