refactor(pl): prrw as a recheckable rule

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the prrw tactic class
(rewrite Pr):

• new module src/phl/rules/bdhoare/EcBdHoarePrFact: the axiom schema
  of the facts on the probabilities of one procedure (mu_eq, mu_sub,
  mu_false, mu_not, mu_or, mu_disjoint, mu_split, mu_ge0, mu_le1, muE,
  mu1_le_eq_mu1, mu_has_le) as the trusted rule t_bdhoare_pr_fact,
  without premise; its node RBdHoarePrFact records the schema and its
  resolved parameters (procedure, arguments, initial memory, events,
  and the binders the fact introduces, so that the fact is a
  deterministic function of the node), checker "bdhoare-pr-fact". The
  pure core regenerates the fact, rechecks the side conditions of the
  schema (events in one memory, the value of mu1_le_eq_mu1 and the
  list of mu_has_le independent of the memory of the event, the
  binders not captured) and compares it with the goal; this replaces
  the opaque `RwPr node closing the cut of the fact;
• the facts are statements on the probability of an event of one
  procedure, the object of the phoare logic (mu1_le_eq_mu1 has a
  phoare premise), hence the module lives in rules/bdhoare/, as
  byphoare and fel do;
• rewrite Pr is derived (t_pr_rewrite, process_pr_rewrite): it
  selects the probability, resolves the parameters and rewrites with
  the cut fact, closed on the spot by the rule;
• byupto (EcEquivUpto) and byequiv (EcEquivDeno) call the new module;
  their TEMPORARY dependencies on EcPhlPrRw are dropped;
• EcPhlPrRw reduced to the legacy entry points, interface unchanged.

Behaviour is preserved: the same facts are generated, hence the same
goals, with the same error messages in the same order (compared with
the reference build on every error path of the new test).

Validation: new test tests/pr-rewrite.ec (every lemma, both
disjunctions, and every error path) passes with the reference build and
this one under EC_RECHECK=1, as do the examples using rewrite Pr,
byupto or byequiv with a bad event; stdlib and unit pass under
EC_RECHECK=1 with no RecheckFailure. The checker, when broken, is
caught only under EC_RECHECK=1 (stdlib: 19 files; unit: 4 files,
tests/pr-rewrite.ec, tests/rw_mu_has_le.ec, tests/deno.ec and
tests/upto.ec).