refactor(pl): exists as recheckable per-logic rules

[strub]

PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the exists tactic class
(elim*, exists* and exlim on program-logic goals, and ecall):

• new trusted rules, eliminating the existentials of a precondition
  (elim*), one per logic and judgement form,
  t_<logic>{S,F}_exists_elim
  (rules/{hoare,ehoare,bdhoare,equiv}/Ec<Logic>Exists):

  forall xs, J [P'] |- J [P]
  

  P' being P with its existential binders pulled to the front
  (EcFol.destr_exists_prenex, through the boolean part of an ehoare
  precondition), as before. The node records the bound on the number of
  binders; the pure builder recomputes the premise from the goal;
  checkers "<logic>{S,F}-exists-elim". The opaque `HlExists node
  is gone.

• exists* / exlim stay derived, now per logic
  (t_<logic>_exists_intro): the consequence rule to
  exists xs, xs = fs /\ P ((exists xs, xs = fs) `|` P for ehoare),
  its premises closed on the spot, then, for exlim, the elimination
  rule. New shared computations in rules/EcPlExists.

• ecall stays derived, now per logic (rules/{hoare,bdhoare,equiv}/
  Ec<Logic>ECall, no trusted rule): the program variables of the
  contract are abstracted by the exists rules, the call is split off by
  the seq rule and closed by the migrated call rule of its logic
  (EcHoareCall, EcBdHoareCall, EcEquivCall); the forward hoare form
  frames the precondition through the hoare split and frame rules. The
  bdhoare form inherits the composite statement of the bdhoare call
  rule (on an empty prefix). Its shared elaboration (typing the
  contract, checking it against the call, abstracting its program
  variables) moves to rules/EcPlECall.

• EcPhlExists is reduced to the dispatchers and adapters; its
  interface is unchanged.

Behaviour is preserved: the goal traces (compile -trace) and the
messages of the 21 files of theories/, tests/ and examples/ using these
tactics are identical with the previous build (20 compile, and
examples/incomplete/oaep fails identically, on a missing theory), and
so are the error messages of the 23 failing tactics of the new test.

Validation: tests/exists-ecall.ec (every rule in every logic and form,
the derived tactics and their error paths; it also passes with the
previous build); stdlib (128 files) and unit (151) under EC_RECHECK=1
with no RecheckFailure. Each checker, when broken, is caught only under
EC_RECHECK=1, on the new test and on the stdlib: hoareS-exists-elim 1
file, hoareF-exists-elim 0, ehoareS-exists-elim 0, ehoareF-exists-elim
0 (unused there), bdhoareS-exists-elim 1, bdhoareF-exists-elim 2,
equivS-exists-elim 7, equivF-exists-elim 1.

Not addressed here: on a phoare goal, ecall with a hoare contract
passes the contract check, then fails with an anomaly (DestrError);
the new test records it as a failure, unchanged.