diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
index 172c397072..dd4d1caa24 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
@@ -43,7 +43,9 @@ private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Exp
   let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
   let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do
     if ys.size < xs.size - 1 then
-      let #[s] ← cases mvarId y | unreachable!
+      let xDecl  ← getLocalDecl xs[ys.size].fvarId!
+      let xDecl' ← getLocalDecl xs[ys.size + 1].fvarId!
+      let #[s] ← cases mvarId y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable!
       go s.mvarId s.fields[1].fvarId! (ys.push s.fields[0])
     else
       let ys := ys.push (mkFVar y)
diff --git a/tests/lean/wf2.lean.expected.out b/tests/lean/wf2.lean.expected.out
index dcfdc188cb..54860035bb 100644
--- a/tests/lean/wf2.lean.expected.out
+++ b/tests/lean/wf2.lean.expected.out
@@ -1,3 +1,3 @@
 wf2.lean:3:8-3:17: error: unsolved goals
-fst✝ snd✝ : Nat
-⊢ fst✝ - 1 < fst✝
+x y : Nat
+⊢ x - 1 < x