Subset_compl:

Mv union_inj from Algebra.Finite_family to union_inj_r.
Add union_inj_l, inter_inj_{l,r}.

Finite_family:
Rename widenF_S_inj -> widenF_S_reg,
       liftF_S_inj -> liftF_S_reg,
       eqAF_0_liftF_S -> extF_liftF_S (modified).
Add and prove widenF_S_compat, eqxFn_equiv,
              widenF_S_nextF_compat, widenF_S_nextF_reg, neqxFn_equiv,
              extF_widenF_S,
              liftF_S_compat, eqxF0_equiv,
              liftF_S_nextF_compat, liftF_S_nextF_reg, neqxF0_equiv.
Mv union_inj to Compl.Subset_compl.union_inj_r.

Finite_dim:
Propagate new API (from Finite_family).