Emit proof steps for the Bool↔Prop bridge

[felipeperet]

Goal: Emit a proof step for the prop-to-bool rewrites on And/Or (propExprToBoolExpr?).

Scope:

B1 = e1 ∧ B2 = e2 ==> true  = (NOP(B1,e1) && NOP(B2,e2))   (if B1 ∨ B2)
B1 = e1 ∧ B2 = e2 ==> false = (e1 || e2)                   (if ¬B1 ∧ ¬B2)
B1 = e1 ∨ B2 = e2 ==> true  = (NOP(B1,e1) || NOP(B2,e2))   (if B1 ∨ B2)
B1 = e1 ∨ B2 = e2 ==> false = (e1 && e2)                   (if ¬B1 ∧ ¬B2)
  where NOP(B,e) = e if B, else !e

Out of scope: the beq-based TODO variants in the file, and the ∧/∨ list reordering.

DoD:

• Each in-scope case pushes its proof step.
• A variable-operand #testOptimize [ ..., proof ] test exercises each case, wired into Tests/Optimize.lean.