phl: migrate seq to the four-layer structure, for every logic

[strub]

Second PR of the src/phl 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.

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.

[strub]

Superseded by #1155 (the branch was renamed to pl/seq, which closed this PR).