Eq hardening: constructor equality

**Goal:** Emit proof steps for the constructor equality reductions in `optimizeEq` (`OptimizeEq.lean`), and flag the remaining reconstructing Eq tests.

**Scope:**
```
C1 = C2 ==> False (distinct constructors, enum types)
nil = [x, y, z] ==> False (list length mismatch)
[z, y] = [x, y, z] ==> False (list structural mismatch)
[f x, y] = [f x, y, z] ==> False
```

**Out of scope:** negation / zero-equals (#180), add/mul cancellation (#181), the `e1 = e2 ==> e2 = e1` reorder, optimizeDecideEq, `EqConstructor_17` (the operand normalization `b + a ==> Nat.add a b` inside a list equality that stays an equality, not a constructor rule).

**DoD:**
- [x] Each in-scope case pushes its proof step.
- [x] A variable-operand `#testOptimize [ ..., proof ]` test exercises each case, wired into `Tests/Optimize.lean`.
- [x] Every remaining reconstructing test in `OptimizeEq.lean` carries the `proof` flag.