Function_compl:

Remove useless lemmas.

Function_sub:
Make some arguments implicit, others explicit.
Add def same_funS.
Add and prove same_funS_{refl,sym,trans},
              RgS{,_gen}_ext, funS_ext, injS_ext,
              surjS_ext, surjS_RgS_equiv,
              canS_ext{_l,_r,}, canS_{injS,surjS}, injS_canS_sym,
              bijS_ext, bijS_RgS, bijS_canS_uniq_{l,r},
              bijS_canS_sym, bijS_canS_bijS.
Rename surjS_equiv -> surjS_RgS_gen_equiv,
       surjS_equiv_alt -> surjS_RgS_equiv_alt.

Finite_family, MonoidComp, Sub_struct, Finite_dim:
Propagate new API (from Function_sub).