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

[strub]

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

• rules/equiv/ecEquivTrans.ml: the two trusted transitivity rules,
  for statements (t_equivS_trans) and procedures (t_equivF_trans),
  documented as inference rules in the .mli: from c1 ~ c2 : P1 ==> Q1,
  c2 ~ c3 : P2 ==> Q2 and the two composition side conditions
  (P => exists intermediate values, P1 /\ P2; Q1 => Q2 => Q), conclude
  c1 ~ c3 : P ==> Q. Each emits a node recording the typed
  intermediate program (memory type and statement, or procedure) and
  the four relations, with a registered checker; the builder takes
  the goal's hyps (it recomputes the variables of the intermediate
  memory and the procedures' memories) and re-checks that the
  relations are stated over the goal's memories.
• transitivity* / replace* (t_equivS_trans_eq, also used by
  outline and rewrite equiv) is a derived form: the rule with
  equality relations, its two side conditions closed on the spot.
• replace involves no position: the pattern only names parts of the
  current program for reuse in the new one, which replaces the whole
  side, so there is no implicit seq-ing or framing to remove.
• EcPhlTrans is reduced to the dispatcher (matching on the goal kind)
  and positional adapters (interface unchanged); the no-op
  FApi.t_low3 wrappers are dropped.

Behaviour is preserved, error messages and their order included.

A new test, tests/transitivity.ec, exercises the statement (both
sides) and procedure forms, transitivity*, replace / replace*
and the error paths; it passes with and without this change. The
stdlib and the unit tests pass under EC_RECHECK=1 with no
RecheckFailure; each checker, when deliberately broken, is caught only
under EC_RECHECK (stdlib: equivS-trans 13 files, equivF-trans 9).