Sub_struct:

Make some arguments explicit.
Add and prove sub_{inj,surj,bij}_{rev,equiv},
              sub_ms_{inj,surj,bij}_{rev,equiv}.
WIP: sub_fun_rev, sub_ms_fun_rev.

P_approx_k:
Remove useless (use replace2F_equiv_def instead of replaceF_switch).