fix: Sym.DSimp.zetaDelta should unfold let-bound variables in head position

[leodemoura]

This PR fixes Sym.DSimp.zetaDelta and Sym.DSimp.zetaDeltaAll so that they unfold a let-bound variable that appears as the head of an application. Previously, dsimp [foo] and dsimp [*] in grind/sym, and the bv_decide normalization passes, left terms such as foo a b untouched when foo := fun x y => x + y was a local definition, while Meta.DSimp reduces them to a + b.

The root cause is that Sym.dsimp intentionally does not visit the head of an application (dsimpAppArgs only traverses the arguments), and both simprocs only matched a bare .fvar. As a result, a let-bound .fvar in argument position was unfolded, but the same .fvar in head position was never seen by the simproc. The fix makes zetaDelta and zetaDeltaAll match on e.getAppFn. When the head is a let-bound .fvar, the result is its value applied to the original arguments, built with mkAppNS to preserve maximal sharing. Beta-reduction of the exposed lambda is still left to the beta simproc, so zetaDeltaAll >> beta yields a + b = b + a for the example above. The doc-string of dsimpAppArgs now states the resulting contract: pre/post simprocs that rewrite heads must match on the whole application.

🤖 Generated with Claude Code