diff --git a/rust/ql/lib/codeql/rust/internal/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/TypeInference.qll
index b8c543ee95b..338135a63c8 100644
--- a/rust/ql/lib/codeql/rust/internal/TypeInference.qll
+++ b/rust/ql/lib/codeql/rust/internal/TypeInference.qll
@@ -1230,7 +1230,7 @@ private module MethodResolution {
       ReceiverIsNotInstantiationOfBlanketLikeSelfParam::argIsNotInstantiationOf(MkMethodCallCand(this,
           derefChain, borrow), impl, _)
       or
-      ReceiverSatisfiesBlanketLikeConstraint::satisfiesNotBlanketConstraint(MkMethodCallCand(this,
+      ReceiverSatisfiesBlanketLikeConstraint::dissatisfiesBlanketConstraint(MkMethodCallCand(this,
           derefChain, borrow), impl)
     }
 
diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
index 2a615418bc2..b88424caa34 100644
--- a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
+++ b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
@@ -138,11 +138,11 @@ module SatisfiesBlanketConstraint<
    * constraint of `impl`.
    */
   pragma[nomagic]
-  predicate satisfiesNotBlanketConstraint(ArgumentType at, ImplItemNode impl) {
+  predicate dissatisfiesBlanketConstraint(ArgumentType at, ImplItemNode impl) {
     exists(ArgumentTypeAndBlanketOffset ato, Trait traitBound |
       ato = MkArgumentTypeAndBlanketOffset(at, _) and
       SatisfiesBlanketConstraintInput::relevantConstraint(ato, impl, traitBound) and
-      SatisfiesBlanketConstraint::satisfiesNotConstraint(ato, TTrait(traitBound))
+      SatisfiesBlanketConstraint::dissatisfiesConstraint(ato, TTrait(traitBound))
     )
   }
 }
diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
index 78b140f91e5..94f227c3a9a 100644
--- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
+++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
@@ -705,10 +705,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       /**
        * Holds if `app` is _not_ a possible instantiation of `constraint`.
        *
-       * This is a monotonic approximation of `not isInstantiationOf(app, abs, constraint)`;
-       * if, for example, `app` has two different types `t1` and `t2` at the same type path,
-       * and `t1` satisfies `constraint` while `t2` does not, then both `isInstantiationOf`
-       * and `isNotInstantiationOf` will hold.
+       * This is an approximation of `not isInstantiationOf(app, abs, constraint)`, but
+       * defined without a negative occurrence of `isInstantiationOf`.
+       *
+       * Due to the approximation, both `isInstantiationOf` and `isNotInstantiationOf`
+       * can hold for the same values. For example, if `app` has two different types `t1`
+       * and `t2` at the same type path, and `t1` satisfies `constraint` while `t2` does
+       * not, then both `isInstantiationOf` and `isNotInstantiationOf` will hold.
        *
        * Dually, if `app` does not have a type at a required type path, then neither
        * `isInstantiationOf` nor `isNotInstantiationOf` will hold.
@@ -1008,6 +1011,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       /**
        * Holds if `tt` does not satisfy `constraint`.
+       *
+       * This predicate is an approximation of `not hasConstraintMention(tt, constraint)`.
        */
       pragma[nomagic]
       private predicate hasNotConstraintMention(HasTypeTree tt, Type constraint) {
@@ -1085,16 +1090,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       /**
        * Holds if the type tree at `tt` does _not_ satisfy the constraint `constraint`.
        *
-       * This is a monotonic approximation of `not satisfiesConstraintType(tt, constraint, _, _)`;
-       * if, for example, `tt` has two different types `t1` and `t2`, and `t1` satisfies
-       * `constraint` while `t2` does not, then both `satisfiesConstraintType` and
-       * `satisfiesNotConstraint` will hold.
+       * This is an approximation of `not satisfiesConstraintType(tt, constraint, _, _)`,
+       * but defined without a negative occurrence of `satisfiesConstraintType`.
+       *
+       * Due to the approximation, both `satisfiesConstraintType` and `dissatisfiesConstraint`
+       * can hold for the same values. For example, if `tt` has two different types `t1`
+       * and `t2`, and `t1` satisfies `constraint` while `t2` does not, then both
+       * `satisfiesConstraintType` and `dissatisfiesConstraint` will hold.
        *
        * Dually, if `tt` does not have a type, then neither `satisfiesConstraintType` nor
-       * `satisfiesNotConstraint` will hold.
+       * `dissatisfiesConstraint` will hold.
        */
       pragma[nomagic]
-      predicate satisfiesNotConstraint(HasTypeTree tt, Type constraint) {
+      predicate dissatisfiesConstraint(HasTypeTree tt, Type constraint) {
         hasNotConstraintMention(tt, constraint) and
         exists(Type t |
           hasTypeConstraint(tt, t, constraint) and