diff --git a/prelude/cf/booleans.lp b/prelude/cf/booleans.lp
index 1f804f08f1fad4f16e7383cbf6b8bcb4a5b8d725..9babe9e7c7b20299620a85c0397abf1962b3e23d 100644
--- a/prelude/cf/booleans.lp
+++ b/prelude/cf/booleans.lp
@@ -4,5 +4,4 @@ definition bool ≔ Prop
 definition false ≔ @prod Type Prop uProp (λ x : @Term Type uProp, x)
 definition true ≔ @Term Prop false ⇒ @Term Prop false
 
-definition bnot (P: @Term Type uProp) ≔ @Term Prop P ⇒ @Term Prop false
-// definition band (P Q: @Term Type uProp) ≔ @Term Prop P ⇒ (bnot (@Term Prop Q))
+definition bnot (P: @Term Type uProp) ≔ @prod Prop Prop P (λ x, false)