Handler Normalization Tactic #

handler_step performs one small normalization pass using the handler_simp set. It is intentionally thin: use it to expose the next handler body or run-shape, then continue with mvcgen, vcstep, rvcstep, or direct proof steps.