fix: simplify Decidable instance neutralization

[zqy1018]

Veil/Util/ReplacingInstances.lean had four simprocs (Depth0/General × actual/expected type). Depth0 differed from General only by leaving unapplied instances (∀ xs, Decidable (p xs)) alone, which nothing relies on, and Depth0WithExpectedType was unused. This PR reduces them to two and makes their proofs independent of unification.

• Two simprocs. neutralizeDecidableInst reads the proposition off the type of the argument and is meant for tactics. neutralizeDecidableInstWithExpectedType reads it off the binder type of the surrounding application and is meant for generated artifacts (LocalRProp/LocalTheoryProp cores, wp_local_eq.pred). Both handle fully applied and unapplied instances, so __veil_neutralize_decidable_inst loses its ! variant.
• Proofs. A replacement is justified by Subsingleton.elim applied directly to both endpoints, and the surrounding congruence uses mkCongrArg/mkCongrFun. Previously mkAppM (including mkFunExt via Simp.Result.addLambdas) re-inferred the endpoints by unification. That unification has to unfold a definition, e.g. a ghost, whenever the instance's type matches the binder type only after unfolding it. The simple private theorem neutralize_Decidable is removed.

Behavior change: tactics that used the old default (Depth0) now also neutralize unapplied instances. Unapplied instances typed as DecidableEq α, DecidablePred p or DecidableRel r, such as module parameters, are still left alone.

[zqy1018]

Seems that something weird happened with stacked PR. Closing it for now.