logic_compl:

Add prop_ext/proof_irrel, aliases for propositional_extensionality/proof_irrelevance.

Function_compl:
Rename bij_ex_uniq -> bij_ex_uniq_equiv.

Function_sub:
Add doc.
Move stuff around.
Modify def bijS.
Rename bijS_alt -> bijS_spec,
       bijS_ex -> bijS_ex_uniq_equiv (modified).
Rm double funS_comp.
Add and prove inj_S_equiv.

ord_compl, Finite_family, MonoidComp, AffineSpace, Sub_struct, Finite_dim,
  multi_index, poly_Lagrange, FE, FE_simplex, FE_LagP:
Propagate new API (from logic_compl, Function_compl, Function_sub).

ord_compl:
Make some arguments implicit.

{Monoid,Group,Ring,ModuleSpace}_compl, AffineSpace:
Add and prove inhabited_fct_{m,g,r,ms,as}.