diff --git a/CHANGELOG.md b/CHANGELOG.md
index 612e45673e..e6ef862be7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -585,6 +585,21 @@ Non-backwards compatible changes
   Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
   ```
 
+### Change to the definition of `Induction.WellFounded.WfRec` (issue #2083)
+
+* Previously, the following definition was adopted
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ y → y < x → P y
+  ```
+  with the consequence that all arguments involving about accesibility and
+  wellfoundedness proofs were polluted by almost-always-inferrable explicit
+  arguments for the `y` position. The definition has now been changed to
+  make that argument *implicit*, as 
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ {y} → y < x → P y
+
 ### Change in the definition of `_≤″_` (issue #1919)
 
 * The definition of `_≤″_` in `Data.Nat.Base` was previously:
diff --git a/README/Data/Nat/Induction.agda b/README/Data/Nat/Induction.agda
index 52b802b2b8..6f47ddc07f 100644
--- a/README/Data/Nat/Induction.agda
+++ b/README/Data/Nat/Induction.agda
@@ -14,6 +14,14 @@ open import Function.Base using (_∘_)
 open import Induction.WellFounded
 open import Relation.Binary.PropositionalEquality
 
+private
+
+  n<′1+n : ∀ {n} → n <′ suc n
+  n<′1+n = ≤′-refl
+
+  n<′2+n : ∀ {n} → n <′ suc (suc n)
+  n<′2+n = ≤′-step ≤′-refl
+
 -- Doubles its input.
 
 twice : ℕ → ℕ
@@ -46,7 +54,7 @@ mutual
   half₂-step = λ
     { zero          _   → zero
     ; (suc zero)    _   → zero
-    ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
+    ; (suc (suc n)) rec → suc (rec n<′2+n)
     }
 
   half₂ : ℕ → ℕ
@@ -92,21 +100,21 @@ half₂-2+ n = begin
 
   half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩
 
-  1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl)  ≡⟨⟩
+  1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n  ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl)          ≡⟨⟩
+        (<′-wellFounded (2 + n)) n<′2+n          ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl)   ≡⟨⟩
+        (acc (<′-wellFounded′ (2 + n))) n<′2+n   ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl)))     ≡⟨⟩
+           (<′-wellFounded′ (2 + n) n<′2+n))     ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (1 + n) n ≤′-refl))               ≡⟨⟩
+           (<′-wellFounded′ (1 + n) n<′1+n))               ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩
@@ -146,7 +154,7 @@ half₁-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 
 half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
@@ -154,6 +162,6 @@ half₂-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 
diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda
index 769c0ccc94..cbc142ff5a 100644
--- a/src/Codata/Musical/Colist/Infinite-merge.agda
+++ b/src/Codata/Musical/Colist/Infinite-merge.agda
@@ -195,7 +195,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
     ... | inj₂ q | P.refl | q≤p =
       Prod.map there
                (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
-               (rec (♭ xss , q) (s≤′s q≤p))
+               (rec (s≤′s q≤p))
 
   to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
 
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 0449279a7d..3c1c25d245 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -195,8 +195,8 @@ true  <? _     = no  (λ())
 <-wellFounded : WellFounded _<_
 <-wellFounded _ = acc <-acc
   where
-    <-acc : ∀ {x} y → y < x → Acc _<_ y
-    <-acc false f<t = acc (λ _ → λ())
+    <-acc : ∀ {x y} → y < x → Acc _<_ y
+    <-acc f<t = acc λ ()
 
 -- Structures
 
diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 60557b142a..3f11c1c3af 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -56,7 +56,7 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
   ... | false = (n % base) ∷ xs
-  ... | true  = aux (wf (n / base) q<n) ((n % base) ∷ xs)
+  ... | true  = aux (wf q<n) ((n % base) ∷ xs)
     where
     q<n : n / base < n
     q<n = m/n<m n base (s<s z<s)
@@ -107,9 +107,8 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base
-  helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
-  helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
-    cons r (rec (suc x) (lem x k (toℕ r)))
+  ... | result zero    r eq = ([ r ] , P.sym eq)
+  ... | result (suc x) r refl = cons r (rec (lem x k (toℕ r)))
 
 ------------------------------------------------------------------------
 -- Showing digits
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index a15287a48f..47e37446bf 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -65,7 +65,7 @@ open WF public using (Acc; acc)
   induct {suc j} (acc rs) (tri< (s≤s i≤j) _ _) _ = Pᵢ⇒Pᵢ₊₁ j P[1+j]
     where
     toℕj≡toℕinjJ = sym $ toℕ-inject₁ j
-    P[1+j] = induct (rs _ (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
+    P[1+j] = induct (rs (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
       (<-cmp i $ inject₁ j) (subst (toℕ i ℕ.≤_) toℕj≡toℕinjJ i≤j)
 
 <-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
@@ -80,8 +80,7 @@ open WF public using (Acc; acc)
 
 private
   acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
-  acc-map {n} (acc rs) = acc λ y y>x →
-    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
+  acc-map (acc rs) = acc λ y>x → acc-map (rs (ℕ.∸-monoʳ-< y>x (toℕ≤n _)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -96,7 +95,7 @@ private
   induct {i} (acc rec) with n ℕ.≟ toℕ i
   ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
-    where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
+    where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Well-foundedness of other (strict) partial orders on Fin
@@ -112,20 +111,20 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 
   spo-wellFounded : ∀ {r} {_⊏_ : Rel (Fin n) r} →
                     IsStrictPartialOrder _≈_ _⊏_ → WellFounded _⊏_
-  spo-wellFounded {_} {_⊏_} isSPO i = go n i pigeon where
+  spo-wellFounded {_} {_⊏_} isSPO i = go n pigeon where
 
     module ⊏ = IsStrictPartialOrder isSPO
 
-    go : ∀ m i →
-         ((xs : Vec (Fin n) m) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
+    go : ∀ m {i} →
+         ({xs : Vec (Fin n) m} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
          Acc _⊏_ i
-    go zero    i k = k [] [-] i
-    go (suc m) i k = acc $ λ j j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑))
+    go zero    k = k [-] _
+    go (suc m) k = acc λ j⊏i → go m λ i∷xs↑ → k (j⊏i ∷ i∷xs↑)
 
-    pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
-    pigeon xs i∷xs↑ =
+    pigeon : {xs : Vec (Fin n) n} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
+    pigeon {xs} i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index d40d078bd3..db9c7286fa 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/src/Data/Graph/Acyclic.agda
@@ -313,7 +313,7 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
     expand n rec (c & g) =
       node (label c)
            (List.map
-              (Prod.map id (λ i → rec (n - suc i) (lemma n i) (g [ i ])))
+              (Prod.map id (λ i → rec (lemma n i) (g [ i ])))
               (successors c))
 
 -- Performs the toTree expansion once for each node.
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index ce16a7528a..3ea0cbb3c0 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -384,15 +384,15 @@ split v as bs p = helper as bs p (<-wellFounded (steps p))
   helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
   helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
   helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
-  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
   helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
   helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
-  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
-  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m<n+m (steps ↭₂) (0<steps ↭₁)))
+  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
   ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
-    (rec _ (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+      (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
 
 ------------------------------------------------------------------------
 -- filter
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 9648718d0d..9abab0823e 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -44,20 +44,21 @@ open PermutationReasoning
 -- Definition
 
 mergePairs : List (List A) → List (List A)
-mergePairs (xs ∷ ys ∷ xss) = merge _≤?_ xs ys ∷ mergePairs xss
+mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
 mergePairs xss             = xss
 
 private
-  length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
+  length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
+                      length (mergePairs zss) < length zss
   length-mergePairs _ _ []              = s<s z<s
-  length-mergePairs _ _ (xss ∷ [])      = s<s (s<s z<s)
-  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
+  length-mergePairs _ _ (xs ∷ [])       = s<s (s<s z<s)
+  length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll []        _               = []
 mergeAll (xs ∷ []) _               = xs
-mergeAll (xs ∷ ys ∷ xss) (acc rec) = mergeAll
-  (mergePairs (xs ∷ ys ∷ xss)) (rec _ (length-mergePairs xs ys xss))
+mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
+  (mergePairs xss) (rec (length-mergePairs xs ys yss))
 
 sort : List A → List A
 sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index c879cec098..abc21e7058 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -294,7 +294,7 @@ m*n/m*o≡n/o m@(suc _) n o = helper (<-wellFounded n)
   ... | no  n≮o = begin-equality
     (m * n) / (m * o)             ≡⟨  m/n≡1+[m∸n]/n (*-monoʳ-≤ m (≮⇒≥ n≮o)) ⟩
     1 + (m * n ∸ m * o) / (m * o) ≡˘⟨ cong (λ v → 1 + v / (m * o)) (*-distribˡ-∸ m n o) ⟩
-    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec (n ∸ o) n∸o<n)) ⟩
+    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec n∸o<n)) ⟩
     1 + (n ∸ o) / o               ≡˘⟨ cong₂ _+_ (n/n≡1 o) refl ⟩
     o / o + (n ∸ o) / o           ≡˘⟨ +-distrib-/-∣ˡ (n ∸ o) (divides 1 ((sym (*-identityˡ o)))) ⟩
     (o + (n ∸ o)) / o             ≡⟨  cong (_/ o) (m+[n∸m]≡n (≮⇒≥ n≮o)) ⟩
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index 2aa87002ca..555a902df6 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -43,7 +43,7 @@ open import Algebra.Definitions {A = ℕ} _≡_ as Algebra
 
 gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
 gcd′ m zero      _         _   = m
-gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n)
+gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec n<m) (m%n<n m n)
 
 gcd : ℕ → ℕ → ℕ
 gcd m n with <-cmp m n
@@ -55,15 +55,15 @@ gcd m n with <-cmp m n
 -- Core properties of gcd′
 
 gcd′[m,n]∣m,n : ∀ {m n} rec n<m → gcd′ m n rec n<m ∣ m × gcd′ m n rec n<m ∣ n
-gcd′[m,n]∣m,n {m} {zero}  rec       n<m = ∣-refl , m ∣0
-gcd′[m,n]∣m,n {m} {suc n} (acc rec) n<m
-  with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m (suc n))
+gcd′[m,n]∣m,n {m} {zero}      rec       n<m = ∣-refl , m ∣0
+gcd′[m,n]∣m,n {m} {n@(suc _)} (acc rec) n<m
+  with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec n<m) (m%n<n m n)
   = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n
 
 gcd′-greatest : ∀ {m n c} rec n<m → c ∣ m → c ∣ n → c ∣ gcd′ m n rec n<m
-gcd′-greatest {m} {zero}  rec       n<m c∣m c∣n = c∣m
-gcd′-greatest {m} {suc n} (acc rec) n<m c∣m c∣n =
-  gcd′-greatest (rec _ n<m) (m%n<n m (suc n)) c∣n (%-presˡ-∣ c∣m c∣n)
+gcd′-greatest {m} {zero}      rec       n<m c∣m c∣n = c∣m
+gcd′-greatest {m} {n@(suc _)} (acc rec) n<m c∣m c∣n =
+  gcd′-greatest (rec n<m) (m%n<n m n) c∣n (%-presˡ-∣ c∣m c∣n)
 
 ------------------------------------------------------------------------
 -- Core properties of gcd
@@ -387,13 +387,13 @@ module Bézout where
     P (m , n) = Lemma m n
 
     gcd″ : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p
-    gcd″ (zero  , n)     rec = Lemma.base n
-    gcd″ (suc m , zero)  rec = Lemma.sym (Lemma.base (suc m))
-    gcd″ (suc m , suc n) rec with compare m n
-    ... | equal m     = Lemma.refl (suc m)
-    ... | less m k    = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
+    gcd″ (zero      , n)     rec = Lemma.base n
+    gcd″ (m@(suc _) , zero)  rec = Lemma.sym (Lemma.base m)
+    gcd″ (m′@(suc m) , n′@(suc n)) rec with compare m n
+    ... | equal m     = Lemma.refl m′
+    ... | less m k    = Lemma.stepˡ $ proj₁ rec (lem₁ k m)
                       -- "gcd (suc m) (suc k)"
-    ... | greater n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)
+    ... | greater n k = Lemma.stepʳ $ proj₂ rec (lem₁ k n) n′
                       -- "gcd (suc k) (suc n)"
 
   -- Bézout's identity can be recovered from the GCD.
diff --git a/src/Data/Nat/Induction.agda b/src/Data/Nat/Induction.agda
index efdd57fe3d..e1554074c4 100644
--- a/src/Data/Nat/Induction.agda
+++ b/src/Data/Nat/Induction.agda
@@ -67,8 +67,8 @@ cRec = build cRecBuilder
 
 <′-wellFounded n = acc (<′-wellFounded′ n)
 
-<′-wellFounded′ (suc n) n <′-base       = <′-wellFounded n
-<′-wellFounded′ (suc n) m (<′-step m<n) = <′-wellFounded′ n m m<n
+<′-wellFounded′ (suc n) <′-base       = <′-wellFounded n
+<′-wellFounded′ (suc n) (<′-step m<n) = <′-wellFounded′ n m<n
 
 module _ {ℓ : Level} where
   open WF.All <′-wellFounded ℓ public
@@ -100,7 +100,7 @@ module _ {ℓ : Level} where
   <-wellFounded-skip : ∀ (k : ℕ) → WellFounded _<_
   <-wellFounded-skip zero    n       = <-wellFounded n
   <-wellFounded-skip (suc k) zero    = <-wellFounded 0
-  <-wellFounded-skip (suc k) (suc n) = acc (λ m _ → <-wellFounded-skip k m)
+  <-wellFounded-skip (suc k) (suc n) = acc λ {m} _ → <-wellFounded-skip k m
 
 module _ {ℓ : Level} where
   open WF.All <-wellFounded ℓ public
diff --git a/src/Data/Nat/Logarithm/Core.agda b/src/Data/Nat/Logarithm/Core.agda
index 6a7cdb21e5..397dd3b3b9 100644
--- a/src/Data/Nat/Logarithm/Core.agda
+++ b/src/Data/Nat/Logarithm/Core.agda
@@ -23,7 +23,7 @@ open import Data.Unit
 ⌊log2⌋ : ∀ n → Acc _<_ n → ℕ
 ⌊log2⌋ 0          _        = 0
 ⌊log2⌋ 1          _        = 0
-⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs _ (⌊n/2⌋<n n′))
+⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs (⌊n/2⌋<n n′))
 
 
 -- Ceil version
@@ -31,7 +31,7 @@ open import Data.Unit
 ⌈log2⌉ : ∀ n → Acc _<_ n → ℕ
 ⌈log2⌉ 0                _        = 0
 ⌈log2⌉ 1                _        = 0
-⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs _ (⌈n/2⌉<n n))
+⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs (⌈n/2⌉<n n))
 
 ------------------------------------------------------------------------
 -- Properties of ⌊log2⌋
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 507dfe0a08..ac598c11a4 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -486,7 +486,7 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 ∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
   where
   rec : ∀ {m} → m < n → m ≢ o
-  rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
+  rec o<n refl = m<n⇒m≢o (s<s o<n) refl
 
 ------------------------------------------------------------------------
 -- A module for reasoning about the _≤_ and _<_ relations
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 742c642d60..96adc9b9e1 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -202,13 +202,13 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
     ×-acc : ∀ {x y} →
             Acc _<₁_ x → Acc _<₂_ y →
             WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y)
-    ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u<x)
-      = acc (×-acc (rec₁ u u<x) (wf₂ v))
-    ×-acc acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
+    ×-acc (acc rec₁) acc₂ (inj₁ u<x)
+      = acc (×-acc (rec₁ u<x) (wf₂ _))
+    ×-acc acc₁ (acc rec₂) (inj₂ (u≈x , v<y))
       = Acc-resp-flip-≈
         (×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
         (u≈x , ≡.refl)
-        (acc (×-acc acc₁ (rec₂ v v<y)))
+        (acc (×-acc acc₁ (rec₂ v<y)))
 
 
 module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index 8c41fdfbd4..944edb4927 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -134,7 +134,8 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     where
 
     <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
-    <-wellFounded {0}     [] = acc λ ys ys<[] → ⊥-elim (xs≮[] ys<[])
+    <-wellFounded {0}     [] = acc λ ys<[] → ⊥-elim (xs≮[] ys<[])
+
     <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs
       where
         <⇒uncons-Lex : {xs ys : Vec A (suc n)} → xs < ys → (×-Lex _≈_ _≺_ _<_ on uncons) xs ys
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 7615c99337..61ba4ded19 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -32,7 +32,7 @@ private
 -- well-founded.
 
 WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
-WfRec _<_ P x = ∀ y → y < x → P y
+WfRec _<_ P x = ∀ {y} → y < x → P y
 
 -- The accessibility predicate: x is accessible if everything which is
 -- smaller than x is also accessible (inductively).
@@ -51,13 +51,13 @@ WellFounded _<_ = ∀ x → Acc _<_ x
 -- Basic properties
 
 acc-inverse : ∀ {_<_ : Rel A ℓ} {x : A} (q : Acc _<_ x) →
-              (y : A) → y < x → Acc _<_ y
-acc-inverse (acc rs) y y<x = rs y y<x
+              WfRec _<_ (Acc _<_) x
+acc-inverse (acc rs) y<x = rs y<x
 
 module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
 
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
-  Acc-resp-flip-≈ respʳ x≈y (acc rec) = acc λ z z<y → rec z (respʳ x≈y z<y)
+  Acc-resp-flip-≈ respʳ x≈y (acc rec) = acc λ z<y → rec (respʳ x≈y z<y)
 
   Acc-resp-≈ : Symmetric _≈_ → _<_ Respectsʳ _≈_ → (Acc _<_) Respects _≈_
   Acc-resp-≈ sym respʳ x≈y wf = Acc-resp-flip-≈ (respʳ ∘ sym) x≈y wf
@@ -68,14 +68,13 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
 module Some {_<_ : Rel A r} {ℓ} where
 
   wfRecBuilder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ {ℓ = ℓ})
-  wfRecBuilder P f x (acc rs) = λ y y<x →
-    f y (wfRecBuilder P f y (rs y y<x))
+  wfRecBuilder P f x (acc rs) = λ y<x → f _ (wfRecBuilder P f _ (rs y<x))
 
   wfRec : SubsetRecursor (Acc _<_) (WfRec _<_)
   wfRec = subsetBuild wfRecBuilder
 
   unfold-wfRec : (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P) {x : A} (q : Acc _<_ x) →
-                 wfRec P f x q ≡ f x (λ y y<x → wfRec P f y (acc-inverse q y y<x))
+                 wfRec P f x q ≡ f x λ y<x → wfRec P f _ (acc-inverse q y<x)
   unfold-wfRec P f (acc rs) = refl
 
 
@@ -96,22 +95,26 @@ module All {_<_ : Rel A r} (wf : WellFounded _<_) ℓ where
 module FixPoint
   {_<_ : Rel A r} (wf : WellFounded _<_)
   (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P)
-  (f-ext : (x : A) {IH IH′ : WfRec _<_ P x} → (∀ {y} y<x → IH y y<x ≡ IH′ y y<x) → f x IH ≡ f x IH′)
+  (f-ext : (x : A) {IH IH′ : WfRec _<_ P x} →
+           (∀ {y} y<x → IH {y} y<x ≡ IH′ y<x) →
+           f x IH ≡ f x IH′)
   where
 
-  some-wfRec-irrelevant : ∀ x → (q q′ : Acc _<_ x) → Some.wfRec P f x q ≡ Some.wfRec P f x q′
-  some-wfRec-irrelevant = All.wfRec wf _
-                                   (λ x → (q q′ : Acc _<_ x) → Some.wfRec P f x q ≡ Some.wfRec P f x q′)
-                                   (λ { x IH (acc rs) (acc rs′) → f-ext x (λ y<x → IH _ y<x (rs _ y<x) (rs′ _ y<x)) })
+  some-wfrec-Irrelevant : Pred A _
+  some-wfrec-Irrelevant x = ∀ q q′ → Some.wfRec P f x q ≡ Some.wfRec P f x q′
+
+  some-wfRec-irrelevant : ∀ x → some-wfrec-Irrelevant x
+  some-wfRec-irrelevant = All.wfRec wf _ some-wfrec-Irrelevant
+    λ { x IH (acc rs) (acc rs′) → f-ext x λ y<x → IH y<x (rs y<x) (rs′ y<x) }
 
   open All wf ℓ
-  wfRecBuilder-wfRec : ∀ {x y} y<x → wfRecBuilder P f x y y<x ≡ wfRec P f y
-  wfRecBuilder-wfRec {x} {y} y<x with wf x
-  ... | acc rs = some-wfRec-irrelevant y (rs y y<x) (wf y)
 
-  unfold-wfRec : ∀ {x} → wfRec P f x ≡ f x (λ y _ → wfRec P f y)
-  unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec
+  wfRecBuilder-wfRec : ∀ {x y} y<x → wfRecBuilder P f x y<x ≡ wfRec P f y
+  wfRecBuilder-wfRec {x} {y} y<x with acc rs ← wf x
+   = some-wfRec-irrelevant y (rs y<x) (wf y)
 
+  unfold-wfRec : ∀ {x} → wfRec P f x ≡ f x λ _ → wfRec P f _
+  unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec
 
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using
@@ -123,7 +126,7 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
                    (<₁⇒<₂ : ∀ {x y} → x <₁ y → x <₂ y) where
 
   accessible : Acc _<₂_ ⊆ Acc _<₁_
-  accessible (acc rs) = acc λ y y<x → accessible (rs y (<₁⇒<₂ y<x))
+  accessible (acc rs) = acc λ y<x → accessible (rs (<₁⇒<₂ y<x))
 
   wellFounded : WellFounded _<₂_ → WellFounded _<₁_
   wellFounded wf = λ x → accessible (wf x)
@@ -134,7 +137,7 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
 module InverseImage {_<_ : Rel B ℓ} (f : A → B) where
 
   accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x
-  accessible (acc rs) = acc λ y fy<fx → accessible (rs (f y) fy<fx)
+  accessible (acc rs) = acc λ fy<fx → accessible (rs fy<fx)
 
   wellFounded : WellFounded _<_ → WellFounded (_<_ on f)
   wellFounded wf = λ x → accessible (wf (f x))
@@ -161,7 +164,7 @@ module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
     trans : ∀ {x y z} (x<y : x <⁺ y) (y<z : y <⁺ z) → x <⁺ z
 
   downwardsClosed : ∀ {x y} → Acc _<⁺_ y → x <⁺ y → Acc _<⁺_ x
-  downwardsClosed (acc rs) x<y = acc λ z z<x → rs z (trans z<x x<y)
+  downwardsClosed (acc rs) x<y = acc λ z<x → rs (trans z<x x<y)
 
   mutual
 
@@ -169,9 +172,9 @@ module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
     accessible acc-x = acc (accessible′ acc-x)
 
     accessible′ : ∀ {x} → Acc _<_ x → WfRec _<⁺_ (Acc _<⁺_) x
-    accessible′ (acc rs) y [ y<x ]         = accessible (rs y y<x)
-    accessible′ acc-x    y (trans y<z z<x) =
-      downwardsClosed (accessible′ acc-x _ z<x) y<z
+    accessible′ (acc rs) [ y<x ]         = accessible (rs y<x)
+    accessible′ acc-x    (trans y<z z<x) =
+      downwardsClosed (accessible′ acc-x z<x) y<z
 
   wellFounded : WellFounded _<_ → WellFounded _<⁺_
   wellFounded wf = λ x → accessible (wf x)
@@ -205,9 +208,9 @@ module Lexicographic {A : Set a} {B : A → Set b}
       ∀ {x y} →
       Acc RelA x → Acc (RelB x) y → (∀ {x} → WellFounded (RelB x)) →
       WfRec _<_ (Acc _<_) (x , y)
-    accessible′ (acc rsA) _    wfB ._ (left  x′<x) = accessible (rsA _ x′<x) wfB
-    accessible′ accA (acc rsB) wfB ._ (right y′<y) =
-      acc (accessible′ accA (rsB _ y′<y) wfB)
+    accessible′ (acc rsA) _    wfB (left  x′<x) = accessible (rsA x′<x) wfB
+    accessible′ accA (acc rsB) wfB (right y′<y) =
+      acc (accessible′ accA (rsB y′<y) wfB)
 
   wellFounded : WellFounded RelA → (∀ {x} → WellFounded (RelB x)) →
                 WellFounded _<_
diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda
index 7c12fa7bcd..e4154d49cd 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive.agda
@@ -80,8 +80,8 @@ module _ (_∼_ : Rel A ℓ) where
   accessible acc[x] = acc (wf-acc acc[x])
     where
     wf-acc : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
-    wf-acc (acc rec) _ [ y∼x ]   = acc (wf-acc (rec _ y∼x))
-    wf-acc acc[x] _ (y∼z ∷ z∼⁺x) = acc-inverse (wf-acc acc[x] _ z∼⁺x) _ [ y∼z ]
+    wf-acc (acc rec) [ y∼x ]   = acc (wf-acc (rec y∼x))
+    wf-acc acc[x] (y∼z ∷ z∼⁺x) = acc-inverse (wf-acc acc[x] z∼⁺x) [ y∼z ]
 
   wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
   wellFounded wf x = accessible (wf x)
diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda
index 72959ac922..c124f98dd8 100644
--- a/src/Relation/Binary/Construct/On.agda
+++ b/src/Relation/Binary/Construct/On.agda
@@ -74,7 +74,7 @@ module _ (f : B → A) where
   trichotomous _ _ compare x y = compare (f x) (f y)
 
   accessible : ∀ {∼ : Rel A ℓ} {x} → Acc ∼ (f x) → Acc (∼ on f) x
-  accessible (acc rs) = acc (λ y fy<fx → accessible (rs (f y) fy<fx))
+  accessible (acc rs) = acc (λ fy<fx → accessible (rs fy<fx))
 
   wellFounded : {∼ : Rel A ℓ} → WellFounded ∼ → WellFounded (∼ on f)
   wellFounded wf x = accessible (wf (f x))
diff --git a/src/Relation/Binary/Rewriting.agda b/src/Relation/Binary/Rewriting.agda
index 10d760e23b..903ab9018e 100644
--- a/src/Relation/Binary/Rewriting.agda
+++ b/src/Relation/Binary/Rewriting.agda
@@ -117,8 +117,8 @@ module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where
         jToInner = proj₁ (proj₂ wcrProof)
         kToInner = proj₂ (proj₂ wcrProof)
 
-        lhs = helper (g _ [ toJ ]) fst jToInner
-        rhs = helper (g _ [ toK ]) snd kToInner
+        lhs = helper (g [ toJ ]) fst jToInner
+        rhs = helper (g [ toK ]) snd kToInner
 
         fromAB = proj₁ (proj₂ lhs)
         fromInnerB = proj₂ (proj₂ lhs)
@@ -129,7 +129,7 @@ module _ {a ℓ} {A : Set a} {_⟶_ : Rel A ℓ} where
         aToInner : _ ⟶₊ innerPoint
         aToInner = starToPlus toJ jToInner
 
-        finalRecursion = helper (g innerPoint aToInner) fromInnerB fromInnerC
+        finalRecursion = helper (g aToInner) fromInnerB fromInnerC
 
         bMidToDest = proj₁ (proj₂ finalRecursion)
         cMidToDest = proj₂ (proj₂ finalRecursion)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Base.agda b/src/Tactic/RingSolver/Core/Polynomial/Base.agda
index 0a027d6d3f..6de64bf839 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Base.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Base.agda
@@ -316,7 +316,7 @@ mutual
 
 ⊟-step : ∀ {n} → Acc _<′_ n → Poly n → Poly n
 ⊟-step (acc wf) (Κ x  ⊐ i≤n) = Κ (- x) ⊐ i≤n
-⊟-step (acc wf) (⅀ xs ⊐ i≤n) = poly-map (⊟-step (wf _ i≤n)) xs ⊐↓ i≤n
+⊟-step (acc wf) (⅀ xs ⊐ i≤n) = poly-map (⊟-step (wf i≤n)) xs ⊐↓ i≤n
 
 ⊟_ : ∀ {n} → Poly n → Poly n
 ⊟_ = ⊟-step (<′-wellFounded _)
@@ -335,12 +335,12 @@ mutual
 
   ⊠-Κ : ∀ {n} → Acc _<′_ n → Carrier → Poly n → Poly n
   ⊠-Κ (acc _ ) x (Κ y  ⊐ i≤n) = Κ (x * y) ⊐ i≤n
-  ⊠-Κ (acc wf) x (⅀ xs ⊐ i≤n) = ⊠-Κ-inj (wf _ i≤n) x xs ⊐↓ i≤n
+  ⊠-Κ (acc wf) x (⅀ xs ⊐ i≤n) = ⊠-Κ-inj (wf i≤n) x xs ⊐↓ i≤n
   {-# INLINE ⊠-Κ #-}
 
   ⊠-⅀ : ∀ {i n} → Acc _<′_ n → Coeff i + → i <′ n → Poly n → Poly n
   ⊠-⅀ (acc wf) xs i≤n (⅀ ys ⊐ j≤n) = ⊠-match  (acc wf) (inj-compare i≤n j≤n) xs ys
-  ⊠-⅀ (acc wf) xs i≤n (Κ y ⊐ _)    = ⊠-Κ-inj (wf _ i≤n) y xs ⊐↓ i≤n
+  ⊠-⅀ (acc wf) xs i≤n (Κ y ⊐ _)    = ⊠-Κ-inj (wf i≤n) y xs ⊐↓ i≤n
 
   ⊠-Κ-inj : ∀ {i}  → Acc _<′_ i → Carrier → Coeff i + → Coeff i *
   ⊠-Κ-inj a x xs = poly-map (⊠-Κ a x) (xs)
@@ -352,7 +352,7 @@ mutual
           → Poly k
           → Poly k
   ⊠-⅀-inj (acc wf) i≤k x (⅀ y ⊐ j≤k) = ⊠-match (acc wf) (inj-compare i≤k j≤k) x y
-  ⊠-⅀-inj (acc wf) i≤k x (Κ y ⊐ j≤k) = ⊠-Κ-inj (wf _ i≤k) y x ⊐↓ i≤k
+  ⊠-⅀-inj (acc wf) i≤k x (Κ y ⊐ j≤k) = ⊠-Κ-inj (wf i≤k) y x ⊐↓ i≤k
 
   ⊠-match : ∀ {i j n}
           → Acc _<′_ n
@@ -362,9 +362,9 @@ mutual
           → Coeff i +
           → Coeff j +
           → Poly n
-  ⊠-match (acc wf) (inj-eq i&j≤n)     xs ys = ⊠-coeffs (wf _ i&j≤n) xs ys               ⊐↓ i&j≤n
-  ⊠-match (acc wf) (inj-lt i≤j-1 j≤n) xs ys = poly-map (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs) (ys) ⊐↓ j≤n
-  ⊠-match (acc wf) (inj-gt i≤n j≤i-1) xs ys = poly-map (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys) (xs) ⊐↓ i≤n
+  ⊠-match (acc wf) (inj-eq i&j≤n)     xs ys = ⊠-coeffs (wf i&j≤n) xs ys               ⊐↓ i&j≤n
+  ⊠-match (acc wf) (inj-lt i≤j-1 j≤n) xs ys = poly-map (⊠-⅀-inj (wf j≤n) i≤j-1 xs) (ys) ⊐↓ j≤n
+  ⊠-match (acc wf) (inj-gt i≤n j≤i-1) xs ys = poly-map (⊠-⅀-inj (wf i≤n) j≤i-1 ys) (xs) ⊐↓ i≤n
 
   ⊠-coeffs : ∀ {n} → Acc _<′_ n → Coeff n + → Coeff n + → Coeff n *
   ⊠-coeffs a (xs) (y ≠0 Δ j & [])   = poly-map (⊠-step′ a y) (xs) ⍓* j
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
index c4e1ef756b..07e157389c 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
@@ -58,10 +58,10 @@ mutual
   ⊠-Κ-hom (acc _)  x (Κ y  ⊐ i≤n) ρ = *-homo x y
   ⊠-Κ-hom (acc wf) x (⅀ xs ⊐ i≤n) ρ =
     begin
-      ⟦ ⊠-Κ-inj (wf _ i≤n) x xs ⊐↓ i≤n ⟧ ρ
-    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i≤n) x xs) i≤n ρ ⟩
-      ⅀?⟦ ⊠-Κ-inj (wf _ i≤n) x xs ⟧ (drop-1 i≤n ρ)
-    ≈⟨ ⊠-Κ-inj-hom (wf _ i≤n) x xs (drop-1 i≤n ρ) ⟩
+      ⟦ ⊠-Κ-inj (wf i≤n) x xs ⊐↓ i≤n ⟧ ρ
+    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i≤n) x xs) i≤n ρ ⟩
+      ⅀?⟦ ⊠-Κ-inj (wf i≤n) x xs ⟧ (drop-1 i≤n ρ)
+    ≈⟨ ⊠-Κ-inj-hom (wf i≤n) x xs (drop-1 i≤n ρ) ⟩
       ⟦ x ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i≤n ρ)
     ∎
 
@@ -94,10 +94,10 @@ mutual
   ⊠-⅀-hom (acc wf) xs i<n (⅀ ys ⊐ j≤n) = ⊠-match-hom (acc wf) (inj-compare i<n j≤n) xs ys
   ⊠-⅀-hom (acc wf) xs i<n (Κ y  ⊐ _) ρ =
     begin
-      ⟦ ⊠-Κ-inj (wf _ i<n) y xs ⊐↓ i<n ⟧ ρ
-    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i<n) y xs) i<n ρ ⟩
-      ⅀?⟦ ⊠-Κ-inj (wf _ i<n) y xs ⟧ (drop-1 i<n ρ)
-    ≈⟨ ⊠-Κ-inj-hom (wf _ i<n) y xs (drop-1 i<n ρ) ⟩
+      ⟦ ⊠-Κ-inj (wf i<n) y xs ⊐↓ i<n ⟧ ρ
+    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i<n) y xs) i<n ρ ⟩
+      ⅀?⟦ ⊠-Κ-inj (wf i<n) y xs ⟧ (drop-1 i<n ρ)
+    ≈⟨ ⊠-Κ-inj-hom (wf i<n) y xs (drop-1 i<n ρ) ⟩
       ⟦ y ⟧ᵣ * ⅀⟦ xs ⟧ (drop-1 i<n ρ)
     ≈⟨ *-comm _ _ ⟩
       ⅀⟦ xs ⟧ (drop-1 i<n ρ) * ⟦ y ⟧ᵣ
@@ -113,10 +113,10 @@ mutual
   ⊠-⅀-inj-hom (acc wf) i<k x (⅀ ys ⊐ j≤k) = ⊠-match-hom (acc wf) (inj-compare i<k j≤k) x ys
   ⊠-⅀-inj-hom (acc wf) i<k x (Κ y ⊐ j≤k) ρ =
     begin
-      ⟦ ⊠-Κ-inj (wf _ i<k) y x ⊐↓ i<k ⟧ ρ
-    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf _ i<k) y x) i<k ρ ⟩
-      ⅀?⟦ ⊠-Κ-inj (wf _ i<k) y x ⟧ (drop-1 i<k ρ)
-    ≈⟨ ⊠-Κ-inj-hom (wf _ i<k) y x (drop-1 i<k ρ) ⟩
+      ⟦ ⊠-Κ-inj (wf i<k) y x ⊐↓ i<k ⟧ ρ
+    ≈⟨ ⊐↓-hom (⊠-Κ-inj (wf i<k) y x) i<k ρ ⟩
+      ⅀?⟦ ⊠-Κ-inj (wf i<k) y x ⟧ (drop-1 i<k ρ)
+    ≈⟨ ⊠-Κ-inj-hom (wf i<k) y x (drop-1 i<k ρ) ⟩
       ⟦ y ⟧ᵣ * ⅀⟦ x ⟧ (drop-1 i<k ρ)
     ≈⟨ *-comm _ _ ⟩
       ⅀⟦ x ⟧ (drop-1 i<k ρ) * ⟦ y ⟧ᵣ
@@ -137,15 +137,15 @@ mutual
         xs′ = ⅀⟦ xs ⟧ (drop-1 (≤′-trans (≤′-step i≤j-1) j≤n) Ρ′)
     in
     begin
-      ⟦ poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys ⊐↓ j≤n ⟧ Ρ′
-    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys) j≤n Ρ′ ⟩
-      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)) ys ⟧ (ρ , Ρ)
-    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf _ j≤n) i≤j-1 xs)
+      ⟦ poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys ⊐↓ j≤n ⟧ Ρ′
+    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys) j≤n Ρ′ ⟩
+      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf j≤n) i≤j-1 xs)) ys ⟧ (ρ , Ρ)
+    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf j≤n) i≤j-1 xs)
                      (_ *_)
                      (*-cong refl)
                      reassoc
                      (distribˡ _)
-                     (λ y → ⊠-⅀-inj-hom (wf _ j≤n) i≤j-1 xs y _)
+                     (λ y → ⊠-⅀-inj-hom (wf j≤n) i≤j-1 xs y _)
                      (zeroʳ _) ys ⟩
        ⅀⟦ xs ⟧ (drop-1 i≤j-1 Ρ) * ⅀⟦ ys ⟧ (ρ , Ρ)
     ≈⟨ ≪* trans-join-coeffs-hom i≤j-1 j≤n xs Ρ′ ⟩
@@ -156,15 +156,15 @@ mutual
         ys′ = ⅀⟦ ys ⟧ (drop-1 (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) Ρ′)
     in
     begin
-      ⟦ poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs ⊐↓ i≤n ⟧ Ρ′
-    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs) i≤n Ρ′ ⟩
-      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)) xs ⟧ (ρ , Ρ)
-    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf _ i≤n) j≤i-1 ys)
+      ⟦ poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs ⊐↓ i≤n ⟧ Ρ′
+    ≈⟨ ⊐↓-hom (poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs) i≤n Ρ′ ⟩
+      ⅀?⟦ poly-map ( (⊠-⅀-inj (wf i≤n) j≤i-1 ys)) xs ⟧ (ρ , Ρ)
+    ≈⟨ poly-mapR ρ Ρ (⊠-⅀-inj (wf i≤n) j≤i-1 ys)
                      (_ *_)
                      (*-cong refl)
                      reassoc
                      (distribˡ _)
-                     (λ x → ⊠-⅀-inj-hom (wf _ i≤n) j≤i-1 ys x _)
+                     (λ x → ⊠-⅀-inj-hom (wf i≤n) j≤i-1 ys x _)
                      (zeroʳ _) xs ⟩
       ⅀⟦ ys ⟧ (drop-1 j≤i-1 Ρ) * ⅀⟦ xs ⟧ (ρ , Ρ)
     ≈⟨ ≪* trans-join-coeffs-hom j≤i-1 i≤n ys Ρ′ ⟩
@@ -174,10 +174,10 @@ mutual
     ∎
   ⊠-match-hom (acc wf) (inj-eq ij≤n) xs ys Ρ =
     begin
-      ⟦ ⊠-coeffs (wf _ ij≤n) xs ys ⊐↓ ij≤n ⟧ Ρ
-    ≈⟨ ⊐↓-hom (⊠-coeffs (wf _ ij≤n) xs ys) ij≤n Ρ ⟩
-      ⅀?⟦ ⊠-coeffs (wf _ ij≤n) xs ys ⟧ (drop-1 ij≤n Ρ)
-    ≈⟨ ⊠-coeffs-hom (wf _ ij≤n) xs ys (drop-1 ij≤n Ρ) ⟩
+      ⟦ ⊠-coeffs (wf ij≤n) xs ys ⊐↓ ij≤n ⟧ Ρ
+    ≈⟨ ⊐↓-hom (⊠-coeffs (wf ij≤n) xs ys) ij≤n Ρ ⟩
+      ⅀?⟦ ⊠-coeffs (wf ij≤n) xs ys ⟧ (drop-1 ij≤n Ρ)
+    ≈⟨ ⊠-coeffs-hom (wf ij≤n) xs ys (drop-1 ij≤n Ρ) ⟩
       ⅀⟦ xs ⟧ (drop-1 ij≤n Ρ) * ⅀⟦ ys ⟧ (drop-1 ij≤n Ρ)
     ∎
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
index 604f02c533..b2a4486d6a 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -42,10 +42,10 @@ open import Tactic.RingSolver.Core.Polynomial.Semantics homo
         ∎
   in
   begin
-    ⟦ poly-map (⊟-step (wf _ i≤n)) xs ⊐↓ i≤n ⟧ ρ′
-  ≈⟨ ⊐↓-hom (poly-map (⊟-step (wf _ i≤n)) xs) i≤n ρ′ ⟩
-    ⅀?⟦ poly-map (⊟-step  (wf _ i≤n)) xs ⟧ (ρ , ρs)
-  ≈⟨ poly-mapR ρ ρs (⊟-step (wf _ i≤n)) -_ (-‿cong) (λ x y → *-comm x (- y) ⟨ trans ⟩ -‿*-distribˡ y x ⟨ trans ⟩ -‿cong (*-comm _ _)) (λ x y → sym (-‿+-comm x y)) (flip (⊟-step-hom (wf _ i≤n)) ρs) (sym neg-zero ) xs ⟩
+    ⟦ poly-map (⊟-step (wf i≤n)) xs ⊐↓ i≤n ⟧ ρ′
+  ≈⟨ ⊐↓-hom (poly-map (⊟-step (wf i≤n)) xs) i≤n ρ′ ⟩
+    ⅀?⟦ poly-map (⊟-step  (wf i≤n)) xs ⟧ (ρ , ρs)
+  ≈⟨ poly-mapR ρ ρs (⊟-step (wf i≤n)) -_ (-‿cong) (λ x y → *-comm x (- y) ⟨ trans ⟩ -‿*-distribˡ y x ⟨ trans ⟩ -‿cong (*-comm _ _)) (λ x y → sym (-‿+-comm x y)) (flip (⊟-step-hom (wf i≤n)) ρs) (sym neg-zero ) xs ⟩
     - ⅀⟦ xs ⟧ (ρ , ρs)
   ∎