diff --git a/CHANGELOG.md b/CHANGELOG.md
index ef9533efc6..e81710a2de 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,9 @@ Minor improvements
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
 
+* As a consequence, the type of `Data.Fin.Base.lower₁` has been correspondingly
+  weakened so that the negated hypothesis `n≢i : n ≢ toℕ i` is marked irrelevant.
+
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda
   README.Data.Fin.Relation.Unary.Top
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index c502512448..6b208a8a55 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -19,7 +19,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction-irr)
 
 private
   variable
@@ -116,8 +116,8 @@ inject≤ {n = suc _} (suc i) m≤n = suc (inject≤ i (ℕ.s≤s⁻¹ m≤n))
 
 -- lower₁ "i" _ = "i".
 
-lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
-lower₁ {zero}  zero    ne = contradiction refl ne
+lower₁ : ∀ (i : Fin (suc n)) → .(n ≢ toℕ i) → Fin n
+lower₁ {zero}  zero    ne = contradiction-irr refl ne
 lower₁ {suc n} zero    _  = zero
 lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
@@ -253,7 +253,7 @@ opposite {suc n} (suc i) = inject₁ (opposite i)
 -- McBride's "First-order unification by structural recursion".
 
 punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
-punchOut {_}     {zero}   {zero}  i≢j = contradiction refl i≢j
+punchOut {_}     {zero}   {zero}  i≢j = contradiction-irr refl i≢j
 punchOut {_}     {zero}   {suc j} _   = j
 punchOut {suc _} {suc i}  {zero}  _   = zero
 punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 48bcf8a5ee..f1062ff8f6 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -49,7 +49,8 @@ open import Relation.Binary.PropositionalEquality as ≡
   using (≡-≟-identity; ≢-≟-identity)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; contradiction-irr)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
@@ -521,30 +522,30 @@ inject!-< {suc n} {suc i} (suc k) = s≤s (inject!-< k)
 -- lower₁
 ------------------------------------------------------------------------
 
-toℕ-lower₁ : ∀ i (p : n ≢ toℕ i) → toℕ (lower₁ i p) ≡ toℕ i
-toℕ-lower₁ {ℕ.zero}  zero    p = contradiction refl p
-toℕ-lower₁ {ℕ.suc m} zero    p = refl
-toℕ-lower₁ {ℕ.suc m} (suc i) p = cong ℕ.suc (toℕ-lower₁ i (p ∘ cong ℕ.suc))
+toℕ-lower₁ : ∀ i .(n≢i : n ≢ toℕ i) → toℕ (lower₁ i n≢i) ≡ toℕ i
+toℕ-lower₁ {ℕ.zero}  zero    0≢0 = contradiction-irr refl 0≢0
+toℕ-lower₁ {ℕ.suc m} zero    _   = refl
+toℕ-lower₁ {ℕ.suc m} (suc i) ne  = cong ℕ.suc (toℕ-lower₁ i (ne ∘ cong ℕ.suc))
 
-lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
+lower₁-injective : ∀ .{n≢i : n ≢ toℕ i} .{n≢j : n ≢ toℕ j} →
                    lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
-lower₁-injective {zero}  {zero}  {_}     {n≢i} {_}   _    = contradiction refl n≢i
-lower₁-injective {zero}  {_}     {zero}  {_}   {n≢j} _    = contradiction refl n≢j
-lower₁-injective {suc n} {zero}  {zero}  {_}   {_}   refl = refl
-lower₁-injective {suc n} {suc i} {suc j} {n≢i} {n≢j} eq   =
+lower₁-injective {zero}  {zero}  {_}     {0≢0} {_}   _  = contradiction-irr refl 0≢0
+lower₁-injective {zero}  {_}     {zero}  {_}   {0≢0} _  = contradiction-irr refl 0≢0
+lower₁-injective {suc n} {zero}  {zero}  {_}   {_}   _  = refl
+lower₁-injective {suc n} {suc i} {suc j} {_}   {_}   eq =
   cong suc (lower₁-injective (suc-injective eq))
 
 ------------------------------------------------------------------------
 -- inject₁ and lower₁
 
-inject₁-lower₁ : ∀ (i : Fin (suc n)) (n≢i : n ≢ toℕ i) →
+inject₁-lower₁ : ∀ (i : Fin (suc n)) .(n≢i : n ≢ toℕ i) →
                  inject₁ (lower₁ i n≢i) ≡ i
-inject₁-lower₁ {zero}  zero     0≢0     = contradiction refl 0≢0
+inject₁-lower₁ {zero}  zero     0≢0     = contradiction-irr refl 0≢0
 inject₁-lower₁ {suc n} zero     _       = refl
 inject₁-lower₁ {suc n} (suc i)  n+1≢i+1 =
   cong suc (inject₁-lower₁ i  (n+1≢i+1 ∘ cong suc))
 
-lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
+lower₁-inject₁′ : ∀ (i : Fin n) .(n≢i : n ≢ toℕ (inject₁ i)) →
                   lower₁ (inject₁ i) n≢i ≡ i
 lower₁-inject₁′ zero    _       = refl
 lower₁-inject₁′ (suc i) n+1≢i+1 =
@@ -554,15 +555,15 @@ lower₁-inject₁ : ∀ (i : Fin n) →
                  lower₁ (inject₁ i) (toℕ-inject₁-≢ i) ≡ i
 lower₁-inject₁ i = lower₁-inject₁′ i (toℕ-inject₁-≢ i)
 
-lower₁-irrelevant : ∀ (i : Fin (suc n)) (n≢i₁ n≢i₂ : n ≢ toℕ i) →
+lower₁-irrelevant : ∀ (i : Fin (suc n)) .(n≢i₁ n≢i₂ : n ≢ toℕ i) →
                     lower₁ i n≢i₁ ≡ lower₁ i n≢i₂
-lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction refl 0≢0
+lower₁-irrelevant {zero}  zero     0≢0 _ = contradiction-irr refl 0≢0
 lower₁-irrelevant {suc n} zero     _   _ = refl
 lower₁-irrelevant {suc n} (suc i)  _   _ =
   cong suc (lower₁-irrelevant i _ _)
 
 inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} →
-                  (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i
+                  .(n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i
 inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j))
 
 ------------------------------------------------------------------------