fix: over-specialized backward rules in vcgen's spec rule cache

[sgraf812]

This PR fixes vcgen failing with Failed to apply rule when the same equality spec matches two different programs within one run, e.g. the equations of a recursive function registered via vcgen [f]: the cached backward rule was specialized to the first matched program and could not be applied to the next one.

The rule built from an equality spec unified the equation's LHS with the goal's program, baking the first program's arguments and dictionaries into a rule that is cached per spec theorem, WP instance and excess argument count. Rule construction now treats equality specs like ⊑ wp specs: it pins only what the cache key determines, namely the monad, the value and predicate types and the WP instance, and leaves the equation's remaining variables, including instance binders, as schematic rule parameters that applying the rule binds against the concrete goal program. Dictionary projections this substitution exposes in the premise program are reduced by the existing head-reduction step before the next spec lookup, which also makes the construction-time dictionary synthesis and projection reduction unnecessary.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-17 11:59:21)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto 79bec6d064d8672cb10864cad3d9fd054b6917ae. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-17 12:27:26)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-17 11:59:22)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 19589be against a104164 are in. No significant results found. @sgraf812

• ✅ build//instructions: -1.3G (-0.01%)

Medium changes (1✅)

• ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction//instructions: -1.1G (-14.42%) (reduced significance based on absolute threshold)

Small changes (1✅, 1🟥)

• ✅ build/module/Lean.PostprocessTraces.StoredTraces//instructions: -8.9M (-0.42%)
• 🟥 vcgen/AddSubCancelSimp/700/vcgen//wall-clock: +50ms (+5.27%)