feat(phl): proc rewrite over ranges and whole statements

[strub]

proc rewrite used to act on exactly one instruction per invocation,
so normalising the constants of a cloned procedure body took one call
per statement, with hand-computed positions for nested branches. The
position is now optional and may be a range:

proc rewrite {2} 3 /=            (* one instruction, deep *)
proc rewrite {2} [2..11] /=      (* a range, deep *)
proc rewrite {2} /=              (* the whole program, deep *)
proc rewrite {2} ^while.1?:[1..1] addzC

All forms recurse into the bodies of if/while/match and apply the
rewrite to every expression (assignment and sampling right-hand sides,
guards, call arguments, raise). In lemma mode, instructions without an
occurrence of the pattern are skipped; the tactic fails only if nothing
was rewritten. One side goal is emitted per rewritten expression and
all are discharged internally.

A single position is the singleton range. This changes the behaviour
of lemma rewrites at an if/while/match position, which used to touch
the guard only; they now also rewrite one occurrence in every body
expression.

Match-arm binders are in scope for the rewrite and are renamed apart
from the proof context in the side goals, so a lemma local sharing a
binder's name does not clash.

The position-less lemma form takes a proof term without a leading @
so that proc rewrite at stays unambiguous.

i_map_expr is now derived from a new i_fold_map_expr that threads
an accumulator and the match-arm locals in scope.

The single-expression t_change is subsumed by the range version; its
only caller, the expression form of proc change, was unreachable from
the grammar and is removed.

[bgregoir]

I think I don't understand the code correctly. So I trust you. The behavior of the tactic is nice. An side remark. I think those kind of tactics will be much simpler to review if it was not in the trusted base. You can implement it by doing a transitivity (or a conseq for hoare/phoare/ehoare) with the new program and then use the generated subgoal to prove the equivalence.