simp still panics with appArg!/appFn! in the non-indexed rewriting path

#14921 fixed the stale-candidate mechanism in simprocCore/dsimprocCore. A
second, independent instance of the same class of bug remains in the non-indexed
rewriting path, and still reproduces on current master (b0ae187bb9).

Reproducer

opaque g : Nat → Nat → Unit
@[reducible] def foo : Nat → Unit := g 0

theorem all_unit (x : Unit) : x = () := Subsingleton.elim _ _

example : foo 1 = () := by
  simp (config := { index := false }) only [all_unit]

Output on b0ae187bb9:

error: Unknown constant `_inhabitedExprDummy`
PANIC at Lean.Expr.appArg! Lean.Expr:937:15: application expected
PANIC at Lean.Expr.appFn! Lean.Expr:933:15: application expected

No Mathlib required, and the command still exits 0 because panics are logged at
info severity.

Cause

Simp.tryTheoremCore in src/Lean/Meta/Tactic/Simp/Rewrite.lean strips
numExtraArgs arguments with the partial accessors:

  let mut extraArgs := #[]
  let mut e := e
  for _ in *...numExtraArgs do
    extraArgs := extraArgs.push e.appArg!
    e := e.appFn!

Here the count and the expression disagree for a different reason than in
#14921: with index := false, getMatchLiberal computes the count from the
reduced form g 0 1, which has two arguments, while the stripping runs on the
raw foo 1, which has one. Nothing rewrites the expression mid-loop, so
#14921's fix does not apply.

As before the damage is not only log noise: panic! returns its Inhabited
fallback, so a dummy Expr reaches elaboration and produces the spurious
Unknown constant error above.

Fix

Guarding this loop is appropriate, since unlike the simproc case there is no
candidate list to re-derive; the mismatch is intrinsic to comparing a reduced
form against a raw one:

  for _ in *...numExtraArgs do
    unless e.isApp do return none
    extraArgs := extraArgs.push e.appArg!
    e := e.appFn!

I have this patched and tested locally and can open a PR with a regression test
if that is wanted. This was the second half of the now-closed #14923; the first
half was superseded by #14921, which is the better fix for that mechanism.

Start in src/Lean/Meta/Tactic/Simp/Rewrite.lean at Simp.tryTheoremCore and reproduce the index := false example from the issue. Ensure the non-indexed rewriting path no longer reaches partial app accessors when the argument count exceeds the raw expression, then add and run a regression test confirming the example produces no panic or spurious error.