feat: when preprocessing for WF, also beta-reduce

both Structural and WF recursion have a preprocess module (since #2818
at least). Back then I found that betareducing in WF, like it happens
for structural, bytes because it would drop `let_fun` annotations, which
are of course worth preserving.

Now that #2973 is landed let's see if we can do it now.

I hope that this fixes an issue where code like
```
theorem size_rev {α} (arr : Array α) (i : Nat) : (rev arr i).size = arr.size := by
  unfold rev
  split
  · rw [size_rev]
    rw [Array.size_swap]
  · rfl
termination_by arr.size - i
decreasing_by simp_wf; omega
```
fails but works with `size_rev _ _`.

It fails due to some lambda-redexes that maybe go away.

(Maybe we can also/additinally/alternatively track down where that redex
is created and use `.beta` instead of `.app`.)

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -81,7 +81,8 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
     return false
 
 def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
-  let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) }
+  let preDefs ← preDefs.mapM fun preDef =>
+    return { preDef with value := (← preprocess preDef.value (preDefs.map (·.declName))) }
   let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do
     for preDef in preDefs do
       addAsAxiom preDef

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -9,6 +9,12 @@ import Lean.Elab.RecAppSyntax
 namespace Lean.Elab.WF
 open Meta
 
+private def shouldBetaReduce (e : Expr) (recFnNames : Array Name) : Bool :=
+  if e.isHeadBetaTarget then
+    e.getAppFn.find? (fun e => recFnNames.any (e.isConstOf ·)) |>.isSome
+  else
+    false
+
 /--
 Preprocesses the expessions to improve the effectiveness of `wfRecursion`.
 
@@ -23,8 +29,13 @@ Preprocesses the expessions to improve the effectiveness of `wfRecursion`.
 Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
 remove `let_fun`-lambdas that contain explicit termination proofs.
 -/
-def preprocess (e : Expr) : CoreM Expr :=
+def preprocess (e : Expr) (recFnNames : Array Name)  : CoreM Expr :=
   Core.transform e
+    (pre := fun e =>
+      if shouldBetaReduce e recFnNames then
+        return .visit e.headBeta
+      else
+        return .continue)
     (post := fun e =>
       match e with
       | .app (.mdata m f) a =>