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; make pp_f_node and pp_opt_f local to t_hi_error
- 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
- Move mk_bind_pvar/glob/pvars/globs to ecLowPhlGoal.ml with type
  annotations
- 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

src/ecLowPhlGoal.ml

@@ -706,6 +706,21 @@ let generalize_mod_ts_inv env modil modir f =
   let res = generalize_mod_right env modir f in
   generalize_mod_left env modil res
 
+(* -------------------------------------------------------------------- *)
+(* Build (ident * form) bindings from generalize_mod_ output:            *)
+(* map quantifier-bound names back to concrete pvar/glob expressions.    *)
+
+let mk_bind_pvar (m : memory) (id : EcIdent.t) ((x, ty) : prog_var * ty) : EcIdent.t * ss_inv =
+  id, f_pvar x ty m
+
+let mk_bind_glob (env : env) (m : memory) (id : EcIdent.t) (x : EcPath.mpath) : EcIdent.t * ss_inv =
+  id, NormMp.norm_glob env m x
+
+let mk_bind_pvars (m : memory) ((bd, pvs) : (EcIdent.t * gty) list * (prog_var * ty) list) : (EcIdent.t * ss_inv) list =
+  List.map2 (fun (id, _) pv -> mk_bind_pvar m id pv) bd pvs
+
+let mk_bind_globs (env : env) (m : memory) ((bd, mps) : (EcIdent.t * gty) list * EcPath.mpath list) : (EcIdent.t * ss_inv) list =
+  List.map2 (fun (id, _) mp -> mk_bind_glob env m id mp) bd mps
 
 (* -------------------------------------------------------------------- *)
 let abstract_info env f1 =