Emit proof steps for the decide-of-equality reductions

**Goal:** Emit proof steps for the decide-of-equality reductions (`optimizeDecideEq` in `OptimizeEq.lean`), acceptance in `DecideEq.lean` plus the `DecideEqTrue`/`DecideEqFalse` cases in `NominalDecide.lean`. `DecideEq.lean` also holds ITE/dite and BEq families, which are separate reductions, so sort those out first.

**Scope:**
```
true = decide' e ==> e
false = decide' e ==> ¬ e
decide' e1 = decide' e2 ==> e1 = e2
decide' e1 = e2 ==> e1 = (true = e2)
(true = p) = (true = q) ==> p = q
```

**Out of scope:** the ITE/dite normalization families (`TrueEqIte` / `FalseEqIte` / `TrueEqDite` / `FalseEqDite`) and the BEq families (`EqBoolBeq` / `EqTrueBeq` / `EqFalseBeq`), which are separate reductions. Also the non-decide Eq hardening (#180, #181).

**DoD:**
- [ ] `DecideEq.lean` split into in-scope decide-of-equality tests vs the ITE/dite and BEq families.
- [ ] Each in-scope decide-of-equality rule pushes its proof step.
- [ ] Every reconstructing in-scope test in `DecideEq.lean` and the `NominalDecide.lean` decide-eq cases carries the `proof` flag.