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