Fix false Valid results from constructor proof fields

[RSoulatIOHK]

Constructor equality can report a false theorem as Valid when structures have proof fields. For example, ProofBox.mk 7 (Or.inl True.intro) ≠ ProofBox.mk 7 (Or.inr True.intro) reduced to True, although Lean proves the equality by rfl.

Treat proof fields as equal before comparing constructor tags, and consume a successful structural comparison so values differing only in proofs simplify to equality. Ordinary data fields still distinguish constructors. The same issue is covered inside lists.

Validation:

• Reproduced the false Valid result on beta bafdd4f7.
• Added a kernel-checked rfl witness, five optimizer regressions, and two negative solver regressions requiring Falsified.
• lake build Blaster Tests.FixedIssues.Issue225 passed.
• lake build Tests.Optimize passed (449 build jobs).

This PR targets beta-lambda-cache-optimization and is the first soundness fix from the branch review.

Fixes #225. Regression: Tests/FixedIssues/Issue225.lean.