PQXDH in Lean

6.4. Design decision🔗

All rewrites target the LHS only via conv_lhs. This avoids the unpredictability of VCV-io's vcstep rw under N, which uses first | conv_lhs | conv_rhs and can modify either side of the equation when both sides have matching structure.