Refactor ecPhlConseq.ml: restructure, deduplicate, document, and annotate

- Split the ~500-line monolithic t_hi_conseq dispatcher into 8
  per-goal-type functions (hoareS/F, bdHoareS/F, ehoareS/F, equivS/F)
  with a thin top-level dispatcher
- Extract shared helpers (t_hi_trivial, t_hi_apply_r, etc.) to module
  level
- Unify three identical gen_conseq_nm variants into a single polymorphic
  one
- Factor shared proof-term processing pipeline into process_conseq_core;
  rename process_conseq_1/2 to process_conseq_hs/ss for clarity
- Extract cond_F_notmod_core / cond_S_notmod_core shared helpers,
  reducing cond_{hoare,bdHoare}{F,S}_notmod to 3-line wrappers
- Remove unnecessary ~recurse indirection from equivS/equivF dispatchers
  (make them directly recursive instead)
- Introduce hi_arg type alias and add type annotations to all top-level
  functions
- Add inference-rule comments to every goal-closing tactic and document
  the processing pipeline, naming conventions, and section structure

Author: strub