diff --git a/src/Lean/Data/Array.lean b/src/Lean/Data/Array.lean
new file mode 100644
index 0000000000..dfac79dc02
--- /dev/null
+++ b/src/Lean/Data/Array.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+import Init.Data.Array
+
+namespace Array
+
+/-!
+This module contains utility functions involving Arrays that are useful in a few places
+of the lean code base, but too specialized to live in `Init.Data.Array`, which arguably
+is part of the public, user-facing standard library.
+-/
+
+/--
+Given an array `a`, runs `f xᵢ xⱼ` for all `i < j`, removes those entries for which `f` returns
+`false` (and will subsequently skip pairs if one element is removed), and returns the array of
+remaining elements.
+
+This can be used to remove elements from an array where a “better” element, in some partial
+order, exists in the array.
+-/
+def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
+    m (Array α) := do
+  let mut removed := Array.mkArray a.size false
+  let mut numRemoved := 0
+  for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
+    unless removed[i]! || removed[j]! do
+      let xi := a[i]'h1.2
+      let xj := a[j]'h2.2
+      let (keepi, keepj) ← f xi xj
+      unless keepi do
+        numRemoved := numRemoved + 1
+        removed := removed.set! i true
+      unless keepj do
+        numRemoved := numRemoved + 1
+        removed := removed.set! j true
+  let mut a' := Array.mkEmpty numRemoved
+  for h : i in [:a.size] do
+    unless removed[i]! do
+      a' := a'.push (a[i]'h.2)
+  return a'
+
+end Array
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 10a9d9d336..7dd66d5d31 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -13,6 +13,7 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Data.Array
 
 namespace Lean.Elab.WF
 open Meta
@@ -165,8 +166,29 @@ private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
   unless remainingGoals.isEmpty do
     Term.reportUnsolvedGoals remainingGoals
 
+/-
+Given an array of MVars, assign MVars with equal type and subsumed local context to each other.
+Returns those MVar that did not get assigned.
+-/
+def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
+  mvars.filterPairsM fun mv₁ mv₂ => do
+    let mvdecl₁ ← mv₁.getDecl
+    let mvdecl₂ ← mv₂.getDecl
+    if mvdecl₁.type == mvdecl₂.type then
+      -- same goals; check contexts.
+        if mvdecl₁.lctx.isSubPrefixOf mvdecl₂.lctx then
+          -- mv₁ is better
+          mv₂.assign (.mvar mv₁)
+          return (true, false)
+        if mvdecl₂.lctx.isSubPrefixOf mvdecl₁.lctx then
+          -- mv₂ is better
+          mv₁.assign (.mvar mv₂)
+          return (false, true)
+    return (true, true)
+
 def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
   let goals ← getMVarsNoDelayed value
+  let goals ← assignSubsumed goals
   goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
     match decrTactic? with
     | none => do
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 9a638da218..1993a745c4 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -1,11 +1,4 @@
 Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
-Tactic is run (ideally only once)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
@@ -15,19 +8,9 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only twice)
-Tactic is run (ideally only once, in most general context)
 Tactic is run (ideally only once, in most general context)
 n : Nat
 ⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
-n : Nat h : n ≠ n ⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
-Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
@@ -39,7 +22,3 @@ h : n ≠ n
 n m : Nat
 ⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
     { fst := Nat.succ n, snd := m }
-n m : Nat
-h : n ≠ n
-⊢ (invImage (fun a => PSigma.casesOn a fun x1 snd => sizeOf x1) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
-    { fst := Nat.succ n, snd := m }