diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5fd46170ba..d36e8d28b0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,10 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
+  weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
+  safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
+
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
   README.Data.Fin.Relation.Unary.Top
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 73876e876c..b1e9425bf2 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -47,11 +47,11 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
-contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr : .A → .(¬ A) → Whatever
 contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 
 contradiction : A → ¬ A → Whatever
-contradiction a = contradiction-irr a
+contradiction a ¬a = contradiction-irr a ¬a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a