Emit proof steps for the hypothesis-driven And/Or reductions + reorder

[felipeperet]

Goal: Emit a proof step for the reductions that consult the hypothesis context, plus the commutative reorder, on And/Or (andPropReduction? / orPropReduction?).

Scope:

e1 ∧ e2 ==> e2 / e1 / False
e1 ∨ e2 ==> True / e2 / e1
e1 ∧ e2 ==> e2 ∧ e1  |  e1 ∨ e2 ==> e2 ∨ e1   (reorder, if e2 <ₒ e1)

Out of scope: the eliminative and implies cases.

DoD:

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