diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
index 479a3069304..37fc0be5a50 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
@@ -96,7 +96,8 @@ public interface SourceElement extends SyntaxElement, EqualsModProperty<SourceEl
      * These are not syntactical equal, therefore false is returned.
      */
     @Override
-    default <V> boolean equalsModProperty(Object o, Property<SourceElement> property, V... v) {
+    default <V> boolean equalsModProperty(Object o, Property<? super SourceElement> property,
+            V... v) {
         if (!(o instanceof SourceElement)) {
             return false;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
index cd06367349d..32429104bdb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
@@ -349,7 +349,7 @@ protected int computeHashCode() {
     }
 
     @Override
-    public <V> boolean equalsModProperty(Object o, Property<JTerm> property, V... v) {
+    public <V> boolean equalsModProperty(Object o, Property<? super JTerm> property, V... v) {
         if (!(o instanceof JTerm other)) {
             return false;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java
index bf5228374b8..2bda6af7c12 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualsModProperty.java
@@ -49,7 +49,7 @@ public interface EqualsModProperty<T> {
      * @param <V> the type of the additional parameters needed by {@code property} for the
      *        comparison
      */
-    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
+    <V> boolean equalsModProperty(Object o, Property<? super T> property, V... v);
 
     /**
      * Computes the hash code according to the given ignored {@code property}.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
index d1d5d30e15a..398937ea196 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
@@ -39,7 +39,7 @@
 
 import org.jspecify.annotations.NonNull;
 
-import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY;
 
 
 public final class UseDependencyContractRule implements BuiltInRule {
@@ -224,7 +224,7 @@ public static boolean isBaseOcc(JTerm focus, JTerm candidate) {
             return false;
         }
         for (int i = 1, n = candidate.arity(); i < n; i++) {
-            if (!(candidate.sub(i).equalsModProperty(focus.sub(i), IRRELEVANT_TERM_LABELS_PROPERTY)
+            if (!(candidate.sub(i).equalsModProperty(focus.sub(i), TERM_LABELS_PROPERTY)
                     || candidate.sub(i).op() instanceof LogicVariable)) {
                 return false;
             }