Complete proof coverage for DecidePropAnd / DecidePropOr

**Goal:** Flag the reconstructing DecidePropAnd/Or tests. The prop-to-bool `And`/`Or` bridge (`propExprToBoolExpr?` in `OptimizeBoolPropBinary.lean`, from #174) already covers most cases. Close the small set that does not reconstruct yet.

**Scope:**
```
Flag the ~39 tests per file that already reconstruct via #174.
Remaining fails to handle:
¬ ((true = e) = (false = e)) (boolEqtoEq? step of optimizeDecideEq is not emitted)
```

**Out of scope:**
- the ITE cases (`if ... then x else y` equalities).
- the `==` / BEq cases.
- the decide' `&&`/`||` regrouping, the nominal decide core, optimizeDecideEq.

**DoD:**
- [ ] The remaining cases carry the `proof` flag once `optimizeDecideEq` emits the `boolEqtoEq?` step.
- [ ] Every reconstructing test in `DecidePropAnd.lean` / `DecidePropOr.lean` carries the `proof` flag.