refactor(pl): true, zero and exfalso as recheckable per-logic rules

[strub]

Fifth PR of the program-logic reorganization stack (see
src/phl/REFACTORING.md). It migrates the rules closing trivially valid
judgements, formerly in EcPhlTAuto; they are axioms of the program
logics (no other rule derives them), so they are trusted:

• rules/hoare/ecHoareTrue.ml: hoare [_ : P ==> true] (every
  postcondition, exceptional ones included, is true);
• rules/ehoare/ecEHoareZero.ml: ehoare [_ : P ==> 0%xr];
• rules/{hoare,bdhoare,equiv}/ecExfalso.ml: a false
  precondition (for bdhoare, with the premise 0%r <= d). ehoare has
  no such rule: its precondition is an expectation, never false.

Each rule comes in statement and procedure form, is documented as an
inference rule in its .mli, and emits a (parameterless) node with a
registered checker; its side condition is part of the subgoal builder,
so the checker re-validates it. EcPhlTAuto keeps its interface, as
adapters and the logic-agnostic exfalso dispatcher. Behaviour is
unchanged.

A new test, tests/true-zero-exfalso.ec, exercises every rule. The
stdlib and the unit tests pass under EC_RECHECK=1 with no
RecheckFailure; each of the ten checkers, when deliberately broken, is
caught only under EC_RECHECK (on the new test; on the stdlib too where
the rule is used there: hoareS-true 14 files, hoareF-true 4, hoare /
bdhoare / equiv exfalso 1 each).