[soundness] Constructor proof fields allow false Valid results

On `beta-lambda-cache-optimization` at `bafdd4f7976037cd7bd8e443df04af096dc5b96e`, constructor comparison treats different proof constructors as evidence of unequal enclosing data. This proves a false statement.

Minimal reproducer (Lean 4.24.0):
```lean
import Blaster
structure ProofBox where
proof : True ∨ True

-- Accepted by Lean's kernel without Blaster: proofs are irrelevant.
example : ProofBox.mk (.inl .intro) = ProofBox.mk (.inr .intro) := rfl

-- Should be Falsified; currently reports Unexpected Valid.
#blaster (only-optimize: 1) (gen-cex: 0) (solve-result: 1)
[ProofBox.mk (.inl .intro) ≠ ProofBox.mk (.inr .intro)]
```

`structEq?` compares `Or.inl` and `Or.inr` as disjoint data constructors when traversing proof fields. The same issue occurs inside lists of structures. Proof fields must be ignored for constructor equality, while ordinary data fields must still distinguish values.

A fixing PR has already been opened as #223; its regression file will be renamed to this issue's number.

Start with the structEq? comparison described in the issue and inspect fixing PR #223, including its regression file after it is renamed. Verify that proof fields are ignored for constructor equality while ordinary data fields and structures inside lists still distinguish unequal values, using the supplied Lean reproducer.

Written by the indexing model from the issue text.