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

[strub]

Second PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md), on top of the recheckable proof-node basis.
It migrates the whole seq tactic class:

• rules/hoare/ecHoareSeq.ml, rules/ehoare/ecEHoareSeq.ml,
  rules/bdhoare/ecBdHoareSeq.ml, rules/equiv/ecEquivSeq.ml: one module
  per logic, each with a rule-arguments record, a node record holding
  the resolved data (split indices, typed assertions and bounds), a
  pure subgoal builder shared by the rule and its registered checker,
  and an elaboration entry taking the parse-tree seq_info. Code
  positions are resolved once in the rule (s_split_index), so the
  checker never redoes code resolution.
• The one-sided equiv form is derived (two-sided rule + conseq) and
  lives in ecEquivSeq.ml without a node of its own. The bdhoare rule
  leaves its non-modification subgoal open; the derived
  t_bdhoare_seq_full used by the tactic then tries to discharge it.
  Both derived forms temporarily depend on the unmigrated EcPhlConseq.
• The seq parse info becomes a record (seq_info); EcPhlSeq is reduced
  to the logic-agnostic dispatcher and the legacy positional adapters,
  so its interface and external callers are unchanged. The no-op
  FApi.t_low* wrappers are dropped.
• Each module's .mli documents its trusted rule as an inference rule
  (premises, conclusion, side conditions, node, checker), separately
  from its derived tactics (with what they expand to) and its
  elaboration entry point.

Behaviour is preserved, except that malformed ehoare / bdhoare seq now
report the same error messages as hoare. Two-sided equiv seq still
types its right position in the left memory (flagged in a comment).

New tests tests/seq-{ehoare,equiv,bdhoare}.ec exercise the rules
directly. The stdlib and the unit tests pass under EC_RECHECK=1 with no
RecheckFailure; for each logic, a deliberately wrong checker is caught
only under EC_RECHECK.