diff --git a/prelude/sets.v b/prelude/sets.v
index 3236b3df0f34c47aa88d21d58aa4d3b9778c1ca0..50e5d9547416ff9e2b89825877ad70d2baf3c224 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -20,7 +20,7 @@ Proof. by split; [split | |]; repeat intro. Qed.
 
 Lemma mkSet_elem_of {A} (f : A → Prop) x : (x ∈ mkSet f) = f x.
 Proof. done. Qed.
-Lemma mkSet_not_elem_of {A} (f : A → Prop) x : (x ∉ mkSet f) = (~f x).
+Lemma mkSet_not_elem_of {A} (f : A → Prop) x : (x ∉ mkSet f) = (¬f x).
 Proof. done. Qed.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.