diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index c28fbbe9d5bd6833e200a93dd95f6dba478b9bd7..bc251fe259fe002c0f858b212c1763e98a433cd0 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -17,6 +17,10 @@ the actual operations that may appear in users' proofs. *)
 Lemma lazy_andb_true (b1 b2 : bool) : b1 &&& b2 = true ↔ b1 = true ∧ b2 = true.
 Proof. destruct b1, b2; intuition congruence. Qed.
 
+Definition negb (b : bool) : bool := if b then false else true.
+Lemma negb_true b : negb b = true ↔ b = false.
+Proof. by destruct b. Qed.
+
 Fixpoint Pos_succ (x : positive) : positive :=
   match x with
   | (p~1)%positive => ((Pos_succ p)~0)%positive
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index ba3090367327c75f7473f4cf1c7c2a96522ea36c..0cfc076234865e9458a0f42fd5328dd36fb20e9e 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -6,7 +6,8 @@ From iris.proofmode Require Import base environments.
     do not reduce e.g. before unification happens in [iApply].*)
 Declare Reduction pm_eval := cbv [
   (* base *)
-  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
+  base.negb base.beq
+  base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom