refactor(pl): fel as a recheckable rule

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the fel tactic class (the
failure-event lemma):

• rules/bdhoare/ecBdHoareFel.ml: the failure-event lemma, concluding

  Pr[f(args) @ &m : ev] <= bd
  

  from the bound on the sum of the step bounds, the post- and
  initialization premises and, for each oracle writing the counter, the
  event or the invariant, the phoare bound and the two hoare premises on
  the counter. The rule-arguments record carries the symbolic
  initialization gap, the node the resolved index; the oracles are not
  recorded: the shared builder recomputes them from the program, and
  re-checks the side condition (after the initialization, the counter,
  the event and the invariant are only written by the oracles), so the
  checker "bdhoare-fel" re-validates it.

• The rule stays stated on the whole body of the procedure (an
  implicit seq at the initialization gap), documented as such in its
  .mli: its conclusion is a probability, for which there is no seq
  rule, and restating it through a judgement on the suffix would change
  its premises.

• EcPhlFel is reduced to adapters onto the new module; its interface
  is unchanged.

Behaviour is preserved: on the new test, the goals after every fel
and the error messages of every failing invocation are identical to
those of the unmodified build.

A new test, tests/fel.ec, exercises the rule (without and with oracle
preconditions and invariant, an oracle reached through another
procedure, a later initialization gap) and its error paths. The stdlib,
the unit tests and the examples using fel pass under EC_RECHECK=1
with no RecheckFailure. The checker, when deliberately broken, is
caught only under EC_RECHECK (on the new test and on the stdlib:
bdhoare-fel 4 files).