DecideBoolBinary: DecideBoolAnd / DecideBoolOr

**Goal:** Emit proof steps for the decide-regrouping in `optimizeDecideBoolAnd` / `optimizeDecideBoolOr` (`OptimizeDecideBoolBinary.lean`). Each first calls `optimizeBoolAnd`/`optimizeBoolOr` (already emitting, #178) and then regroups decide' atoms via `decideOpDecide?` — the regrouping is the new emission work.

**Scope:**
```
decide' e1 && decide' e2 ==> decide' (e1 ∧ e2) [decide'_and_decide']
decide' e1 && e2 | e2 && decide' e1 ==> decide' (e1 ∧ true = e2) [decide'_and_bool / bool_and_decide']
(dual reductions for ||)
```

**Out of scope:** the inner Bool `&&`/`||` reductions themselves (`!p && p ==> False` etc., already emit via #178; here they may just need flags or reveal a replay-composition issue), the nominal decide core and the bool-not/decide bridge, the prop-to-bool bridge (`propExprToBoolExpr?`), optimizeDecideEq.

**DoD:**
- [ ] Each regrouping sub-case pushes its proof step.
- [ ] A `#testOptimize [ ..., proof ]` test exercises each, wired into `Tests/Optimize.lean`.
- [ ] Every reconstructing test in `DecideBoolAnd.lean` / `DecideBoolOr.lean` carries the `proof` flag.