{,n}eqx{,2}F, unfunF/maskPF, insert{,2}F/skip{,2}F/replace{,2}F,
  filter_{,n}eqF{_gen,}, splitF_eqF{_gen,}.
And also for some lemmas.
Add notations {insertF,skipF,replaceF}{0,max}, {,n}eqxF{0,max}.

       or_distr_{l,r} -> or_and_{l,r}.

                  *_distr_{l,r} -> *_plus_{r,l},
                  scalF_sum_{l,r}{l,r} -> scalF_sum_{r,l}{l,r},

Proof of aff_indep_decomp_uniq_rev.

                   lin_basis_aff_basis{,_rev,_equiv}.

    lin_indep_aff_indep{,_rev,_equiv}.

Add sum_skipF_compat, sum_eqxF_reg, sum_skipF_reg.

    fct_lm_gather_ms, am_gather{_equiv,,_rev}_ms (proofs redone, why?)

Rename lm_scatter <-> lm_scatter_rev.

Rename am_scatter <-> am_scatter_rev.

Proof of insertF_am.

Add LagPd1_ref_kron_vtx, LagPd1_ref_vtx_skipF.
Proof of Hface_ref_is_Ker.

Rename LagPd1_ref_kron_vtx_r -> LagPd1_ref_kron_vtx.

    T_geom_assoc, T_geom_scal_ref,
    sub_vtxF, sub_vtx_refF,
    sub_nodeF, sub_node_ref, sub_node_ref_eq, T_geom_sub_nodeF.
Simplify proof of sub_node_eq.