diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean
index a3fd604b0b..5df6fb7d9c 100644
--- a/src/Lean/Util/Recognizers.lean
+++ b/src/Lean/Util/Recognizers.lean
@@ -49,6 +49,11 @@ namespace Expr
 @[inline] def not? (p : Expr) : Option Expr :=
   p.app1? ``Not
 
+@[inline] def notNot? (p : Expr) : Option Expr :=
+  match p.not? with
+  | some p => p.not?
+  | none => none
+
 @[inline] def and? (p : Expr) : Option (Expr × Expr) :=
   p.app2? ``And