Function_compl:

Add and prove Rg_compl.

Finite_family:
Generalize castF_eq_sym to any type.
Modify def extendPF.
Rename extendPF_unfunF -> extendPF_unfunF_neq.
Add and prove funF_neq, unfunF_neq,
              extendPF_funF, extendPF_funF_neq,
              extendPF_unfunF{,_rev}, extendPF_equiv,
              len_neqF_funF, filter_neqF_gen_funF.
WIP: filterPF_funF (was filterPF_ext_r_glop),
     filterPF_unfunF (was filterPF_extendPF).