fix: reduce Eq.rec when mvars are present

src/Lean/Meta/WHNF.lean

@@ -125,8 +125,6 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorTypeI := majorType.getAppFn
   if !majorTypeI.isConstOf recVal.getMajorInduct then
     return major
-  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
-    return major
   else do
     let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure major
     let newType ← inferType newCtorApp

tests/lean/6562.lean

@@ -0,0 +1,24 @@
+/-! Patterns with metavariables should still satisfy defeqs -/
+
+example : (x : Nat) → (Eq.refl x).symm.ndrec (motive := fun _ => Bool) false = false → Unit
+  | _, rfl => ()
+
+inductive Mem (a : α) : List α → Type
+  | head (as : List α) : Mem a (a::as)
+  | tail (b : α) {as : List α} : Mem a as → Mem a (b::as)
+
+def del : @Mem α a as → List α
+  | .head as => as
+  | .tail b mem => b :: del mem
+
+def memOfDel : (mem : Mem c as) → Mem a (del mem) → Mem a as
+  | .head _, mem => .tail _ mem
+  | .tail _ mem, .head _ => .head _
+  | .tail _ mem, .tail _ mem' => .tail _ (memOfDel mem mem')
+
+def memOfDel' : (mem : Mem c as) → Mem a (del mem) → Mem a as
+  | .head _, mem => .tail _ mem
+  | .tail b mem, (mem' : Mem a (b :: del mem)) =>
+    match mem' with
+    | .head _ => .head _
+    | .tail _ mem' => .tail _ (memOfDel' mem mem')