diff --git a/FEM/Algebra/AffineSpace.v b/FEM/Algebra/AffineSpace.v
index e4f9541d93a9f32054671a602b8fffad0d0461c6..7fe68c58fe8f3ae887b879e7ce72b25fd84008d7 100644
--- a/FEM/Algebra/AffineSpace.v
+++ b/FEM/Algebra/AffineSpace.v
@@ -101,6 +101,9 @@ Variable E : AffineSpace V.
 Lemma inhabited_as : inhabited E.
 Proof. apply (AffineSpace.ax0 _ _ (AffineSpace.class V _)). Qed.
 
+Lemma inhabited_fct_as : forall {T : Type}, inhabited (T -> E).
+Proof. intros; apply fun_to_nonempty_compat, inhabited_as. Qed.
+
 Definition point_of_as : E := elem_of inhabited_as.
 
 End AffineSpace_Facts0.
@@ -119,7 +122,7 @@ Lemma vect_l_bij_ex : forall (A : E) u, exists! B, A --> B = u.
 Proof. apply AffineSpace.ax2. Qed.
 
 Lemma vect_l_bij : forall (A : E), bijective (vect A).
-Proof. intros; apply bij_ex_uniq, vect_l_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, vect_l_bij_ex. Qed.
 
 Lemma vect_zero : forall (A : E), A --> A = 0.
 Proof.
@@ -149,7 +152,7 @@ move=> A' /opp_eq; rewrite -vect_sym; apply HA2.
 Qed.
 
 Lemma vect_r_bij : forall (B : E), bijective (vect^~ B).
-Proof. intros; apply bij_ex_uniq, vect_r_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, vect_r_bij_ex. Qed.
 
 Lemma vect_l_eq : forall (A B1 B2 : E), B1 = B2 -> A --> B1 = A --> B2.
 Proof. intros; subst; easy. Qed.
@@ -295,7 +298,7 @@ intros A; apply (bij_can_bij (vect_l_bij A)); apply transl_correct_l.
 Qed.
 
 Lemma transl_l_bij_ex : forall (A B : E), exists! u, A +++ u = B.
-Proof. intros; apply bij_ex_uniq, transl_l_bij. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, transl_l_bij. Qed.
 
 Lemma transl_r_bij_ex : forall u (B : E), exists! A, A +++ u = B.
 Proof.
@@ -305,7 +308,7 @@ intros A; rewrite transl_opp_equiv; easy.
 Qed.
 
 Lemma transl_r_bij : forall u, bijective (transl^~ u : E -> E).
-Proof. intros; apply bij_ex_uniq, transl_r_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, transl_r_bij_ex. Qed.
 
 Lemma vect_transl : forall (O : E) u v, (O +++ u) --> (O +++ v) = v - u.
 Proof.
@@ -657,7 +660,7 @@ apply (vect_l_inj O); rewrite mapF_correct -vectF_correct HB; easy.
 Qed.
 
 Lemma vectF_l_bij : forall {n} (O : E), bijective (@vectF _ _ _ n O).
-Proof. intros; apply bij_ex_uniq, vectF_l_bij_ex. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, vectF_l_bij_ex. Qed.
 
 Lemma vectF_zero : forall {n} (O : E), vectF O (constF n O) = 0.
 Proof. intros; apply extF; intro; apply vect_zero. Qed.
@@ -875,7 +878,7 @@ intros n O; apply (bij_can_bij (vectF_l_bij O)); apply translF_vectF.
 Qed.
 
 Lemma translF_l_bij_ex : forall {n} O (A : 'E^n), exists! u, translF O u = A.
-Proof. intros; apply bij_ex_uniq, translF_l_bij. Qed.
+Proof. intros; apply bij_ex_uniq_equiv, translF_l_bij. Qed.
 
 Lemma translF_inj_equiv :
   forall {n} (O : E) (u : 'V^n), injective (translF O u) <-> injective u.
diff --git a/FEM/Algebra/Finite_dim.v b/FEM/Algebra/Finite_dim.v
index 378e9de02ea8d0b51085c3c0c09d460ca8396f08..b8718b69e48c2ca07604538d1f3f0acfbc15569d 100644
--- a/FEM/Algebra/Finite_dim.v
+++ b/FEM/Algebra/Finite_dim.v
@@ -1501,7 +1501,7 @@ rewrite W; apply is_linear_mapping_is_basis_compat; try easy.
 apply is_linear_mapping_bij_compat; try easy.
 apply compatible_ms_image; try easy.
 apply compatible_ms_fullset.
-apply (bijS_injS inhabited_ms fullset).
+apply (bijS_injS fullset).
 replace (image fs fullset) with (@fullset PIs).
 apply bij_S_equiv; try apply inhabited_ms.
 apply f_inv_bij.
diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index d4d8a06d8f4acce7b2c2647062c4638651d357b9..9603b4d65c2513c2ce2da8df33472ebcc4a2efb1 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -64,7 +64,7 @@ Qed.
 Lemma PF_dec_l : forall (H : PAF P), PF_dec = left H.
 Proof.
 intros H1; destruct PF_dec as [H2 | H2].
-f_equal; apply proof_irrelevance.
+f_equal; apply proof_irrel.
 contradict H1; apply not_all_ex_not_equiv; easy.
 Qed.
 
@@ -72,7 +72,7 @@ Lemma PF_dec_r : forall (H : PEF (notF P)), PF_dec = right H.
 Proof.
 intros H1; destruct PF_dec as [H2 | H2].
 contradict H2; apply not_all_ex_not_equiv; easy.
-f_equal; apply proof_irrelevance.
+f_equal; apply proof_irrel.
 Qed.
 
 End FF_Def1a.
@@ -1685,7 +1685,7 @@ Proof.
 intros n1 n2 f A1 x0 Hf; apply extF; intros i2; unfold neqF;
     destruct (unfunF_correct A1 x0 i2 Hf) as [[i1 [<- ->]] | [Hi2 ->]].
 rewrite (unfunF_correct_l _ i1); easy.
-rewrite unfunF_correct_r; [apply propositional_extensionality |]; easy.
+rewrite unfunF_correct_r; [apply prop_ext |]; easy.
 Qed.
 
 End FunF_Facts.
@@ -4676,7 +4676,8 @@ Proof. intros; rewrite filterPF_splitF castF_id lastF_concatF; easy. Qed.
 Lemma lenPF_permutF :
   forall {n} {p} {P : 'Prop^n}, injective p -> lenPF (permutF p P) = lenPF P.
 Proof.
-intros n p P Hp; apply (bijS_eq_card p), injS_surjS_bijS;
+intros n p P Hp; destruct n as [|n]; [rewrite !lenPF_nil; easy |].
+apply (bijS_eq_card p), (injS_surjS_bijS I_S_is_nonempty);
     [apply funS_correct; easy | move=>> _ _; apply Hp |].
 intros i Hi; exists (f_inv (injF_bij Hp) i); unfold permutF;
     rewrite f_inv_correct_r; easy.
diff --git a/FEM/Algebra/Group_compl.v b/FEM/Algebra/Group_compl.v
index 35ae876bba440c3920e6113ed603ebcaf43b4147..a5c716af18f12588f9d6a4c5bf60eba0ab9e6ada 100644
--- a/FEM/Algebra/Group_compl.v
+++ b/FEM/Algebra/Group_compl.v
@@ -46,6 +46,9 @@ Context {G : AbelianGroup}.
 Lemma inhabited_g : inhabited G.
 Proof. apply inhabited_m. Qed.
 
+Lemma inhabited_fct_g : forall {T : Type}, inhabited (T -> G).
+Proof. intros; apply inhabited_fct_m. Qed.
+
 Lemma plus_compat_l_equiv : forall x x1 x2 : G, x1 = x2 <-> x + x1 = x + x2.
 Proof. intros; split; [apply plus_compat_l | apply plus_reg_l]. Qed.
 
diff --git a/FEM/Algebra/ModuleSpace_compl.v b/FEM/Algebra/ModuleSpace_compl.v
index f0c4dd9196911f07bffb2db6ddfb19bdd9bb1640..fec3c54e1de22c70a9e6a426a583b8770276d655 100644
--- a/FEM/Algebra/ModuleSpace_compl.v
+++ b/FEM/Algebra/ModuleSpace_compl.v
@@ -56,6 +56,9 @@ Proof. intros HK u; rewrite -(scal_one u) (HK 1) scal_zero_l; easy. Qed.
 Lemma inhabited_ms : inhabited E.
 Proof. apply inhabited_g. Qed.
 
+Lemma inhabited_fct_ms : forall {T : Type}, inhabited (T -> E).
+Proof. intros; apply inhabited_fct_g. Qed.
+
 Lemma scal_compat :
   forall a b (u v : E), a = b -> u = v -> scal a u = scal b v.
 Proof. intros; f_equal; easy. Qed.
diff --git a/FEM/Algebra/MonoidComp.v b/FEM/Algebra/MonoidComp.v
index bac09dfc678b7fe30675c7f4042b99ea54789de8..4338050dc7f9727f260566edb412f8b1659f67b7 100644
--- a/FEM/Algebra/MonoidComp.v
+++ b/FEM/Algebra/MonoidComp.v
@@ -217,7 +217,7 @@ Lemma comp_n_funS :
 Proof.
 intros n f Hf; induction n as [|n Hn];
     [rewrite comp_n_nil; [apply funS_id | easy] | rewrite comp_n_ind_l].
-apply (funS_comp PE); [apply Hn; unfold liftF_S |]; easy.
+apply funS_comp_compat with PE; [apply Hn; unfold liftF_S |]; easy.
 Qed.
 
 Context {n : nat}.
@@ -295,7 +295,7 @@ intros n f j Hf; induction n as [|n Hn];
     [rewrite comp_n_part_nil; [apply funS_id | easy] |].
 destruct (ord_eq_dec j ord0) as [Hj0 | Hj0];
     [rewrite (comp_n_part_0 _ _ Hj0); apply funS_id |].
-rewrite comp_n_part_ind_l; apply (funS_comp PE); [apply Hn |].
+rewrite comp_n_part_ind_l; apply funS_comp_compat with PE; [apply Hn |].
 intros; apply (widenF_liftF_S_P_compat _ Hj0 Hf); easy.
 apply (widenF_0_P_compat Hj0 Hf).
 Qed.
diff --git a/FEM/Algebra/Monoid_compl.v b/FEM/Algebra/Monoid_compl.v
index 4e7f0c603f5ff1232d2b29c39a21978d0d280faa..ee6ffdda2814f4f8a65c061012ec308dfde23ae0 100644
--- a/FEM/Algebra/Monoid_compl.v
+++ b/FEM/Algebra/Monoid_compl.v
@@ -62,6 +62,9 @@ Context {G : AbelianMonoid}.
 Lemma inhabited_m : inhabited G.
 Proof. apply (inhabits 0). Qed.
 
+Lemma inhabited_fct_m : forall {T : Type}, inhabited (T -> G).
+Proof. intros; apply fun_to_nonempty_compat, inhabited_m. Qed.
+
 Lemma plus_comm : forall x y : G, x + y = y + x.
 Proof. apply AbelianMonoid.ax1. Qed.
 
diff --git a/FEM/Algebra/Ring_compl.v b/FEM/Algebra/Ring_compl.v
index b627fa1d01a7b8b916d5566420fdf1304d9caed4..dd6d55e0d3e5aacacb664413c872a8ac79cdcad6 100644
--- a/FEM/Algebra/Ring_compl.v
+++ b/FEM/Algebra/Ring_compl.v
@@ -145,6 +145,9 @@ Context {K : Ring}.
 Lemma inhabited_r : inhabited K.
 Proof. apply inhabited_g. Qed.
 
+Lemma inhabited_fct_r : forall {T : Type}, inhabited (T -> K).
+Proof. intros; apply inhabited_fct_g. Qed.
+
 Lemma one_is_zero : (1 : K) = 0 -> zero_struct K.
 Proof. intros H x; rewrite -(mult_one_l x) H mult_zero_l; easy. Qed.
 
diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index c62b12459fd346268a045fd0a273e827c7ce74c5..144e8768a5b12cf814afde1bbd733fbe7f7f575f 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -57,7 +57,7 @@ Proof. apply f_equal. Qed.
 
 Lemma val_inj : forall (x y : sub_struct HPT), val x = val y -> x = y.
 Proof.
-intros [x Hx] [y Hy]; simpl; intros; subst; f_equal; apply proof_irrelevance.
+intros [x Hx] [y Hy]; simpl; intros; subst; f_equal; apply proof_irrel.
 Qed.
 
 Lemma mk_sub_eq :
diff --git a/FEM/Algebra/ord_compl.v b/FEM/Algebra/ord_compl.v
index 45d03db40f557e8c53ee29876769656d6d06559d..01bb4516034d0307d97f16a4391422a5905c04e9 100644
--- a/FEM/Algebra/ord_compl.v
+++ b/FEM/Algebra/ord_compl.v
@@ -158,7 +158,7 @@ Section Ord_compl1.
 Lemma I_0_is_empty : ~ inhabited 'I_0.
 Proof. intros [[n Hn]]; easy. Qed.
 
-Lemma I_S_is_nonempty : forall n, inhabited 'I_n.+1.
+Lemma I_S_is_nonempty : forall {n}, inhabited 'I_n.+1.
 Proof. intros; apply (inhabits ord0). Qed.
 
 Lemma fun_from_I_S_to_I_0_is_empty : forall n, ~ inhabited ('I_{n.+1,0}).
@@ -633,6 +633,7 @@ Section Fun_ord2.
 (* More basic properties of functions on ordinals. *)
 
 Context {T1 T2 : finType}.
+
 Context {P1 : pred T1}.
 Context {P2 : pred T2}.
 
@@ -647,19 +648,18 @@ Definition fun_sub (Hf : funS P1 P2 f) : {x1 | P1 x1} -> {x2 | P2 x2} :=
     exist _ x2 Hx2.
 
 Lemma bijS_bijF_sub :
-  forall (Hf : bijS P1 P2 f), bijective (fun_sub (proj1 Hf)).
+  forall (Hf : bijS P1 P2 f), bijective (fun_sub (bijS_funS Hf)).
 Proof.
-intros [Hf1 Hf2]; apply bij_ex_uniq.
+intros Hf1; apply bij_ex_uniq_equiv; destruct (bijS_ex_uniq Hf1) as [_ Hf2].
 intros [x2 Hx2]; destruct (Hf2 x2 Hx2) as [x1 [[Hx1a Hx1b] Hx1c]].
 exists (exist _ x1 Hx1a); split; unfold fun_sub; simpl.
-(* *)
 apply eq_exist; easy.
-(* *)
 move=> [y1 Hy1a] /= Hy1b; apply eq_sig_fst in Hy1b.
 apply eq_exist, Hx1c; split; easy.
 Qed.
 
-Lemma bijS_eq_card : bijS P1 P2 f -> #|[ pred x | P1 x ]| = #|[ pred x | P2 x ]|.
+Lemma bijS_eq_card :
+  bijS P1 P2 f -> #|[ pred x1 | P1 x1 ]| = #|[ pred x2 | P2 x2 ]|.
 Proof.
 move=>> Hf; rewrite -2!card_sig; apply (bij_eq_card (bijS_bijF_sub Hf)).
 Qed.
@@ -1670,7 +1670,7 @@ Proof. intros; apply (inj_comp lift_inj), cast_ord_inj. Qed.
 
 Lemma insert_ord_compat_P :
   forall {n} {i0 i : 'I_n.+1} (H H' : i <> i0), insert_ord H = insert_ord H'.
-Proof. intros; f_equal; apply proof_irrelevance. Qed.
+Proof. intros; f_equal; apply proof_irrel. Qed.
 
 Lemma skip_insert_ord :
   forall {n} {i0 i : 'I_n.+1} (H : i <> i0), skip_ord i0 (insert_ord H) = i.
@@ -1870,7 +1870,7 @@ Lemma insert_f_ord_correct_r :
     insert_f_ord p i0 i = skip_ord i0 (p (insert_ord H)).
 Proof.
 intros; unfold insert_f_ord; destruct (ord_eq_dec _ _);
-    [easy | repeat f_equal; apply proof_irrelevance].
+    [easy | repeat f_equal; apply proof_irrel].
 Qed.
 
 (** Definition and properties of extend_f_S. *)
@@ -1890,7 +1890,7 @@ Lemma extend_f_S_correct_r :
     extend_f_S p i = widen_S (p (narrow_S H)).
 Proof.
 intros; unfold extend_f_S; destruct (ord_eq_dec _ _);
-    [easy | repeat f_equal; apply proof_irrelevance].
+    [easy | repeat f_equal; apply proof_irrel].
 Qed.
 
 End Skip_Insert_ord.
@@ -2095,7 +2095,7 @@ Lemma insert2_ord_compat_P :
   forall {n} {i0 i1 i : 'I_n.+2}
       (H H' : i1 <> i0) (H0 H0' : i <> i0) (H1 H1' : i <> i1),
     insert2_ord H H0 H1 = insert2_ord H' H0' H1'.
-Proof. intros; f_equal; apply proof_irrelevance. Qed.
+Proof. intros; f_equal; apply proof_irrel. Qed.
 
 Lemma insert2_ord_sym :
   forall {n} {i0 i1 i : 'I_n.+2}
@@ -2453,8 +2453,10 @@ Lemma lenPF_ind_l_in :
   forall {n} {P : 'I_n.+1 -> Prop},
     P ord0 -> lenPF P = 1 + lenPF (fun i => P (lift_S i)).
 Proof.
-move=> n P /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
-apply sym_eq, (bijS_eq_card lift_S), injS_surjS_bijS.
+intros n P; destruct n as [|n];
+    [intros HP; rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
+move=> /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
+apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty).
 (* *)
 apply funS_correct; intro; destruct (pselect _); [| easy].
 intros _; apply /andP; split;
@@ -2478,7 +2480,8 @@ Lemma lenPF_ind_l_out :
   forall {n} {P : 'I_n.+1 -> Prop},
     ~ P ord0 -> lenPF P = lenPF (fun i => P (lift_S i)).
 Proof.
-intros; apply sym_eq, (bijS_eq_card lift_S), injS_surjS_bijS;
+intros n P HP; destruct n as [|n]; [rewrite (lenPF1_out HP) lenPF_nil; easy |].
+apply sym_eq, (bijS_eq_card lift_S), (injS_surjS_bijS I_S_is_nonempty);
     [apply funS_correct; easy | move=>> _ _; apply: lift_inj |].
 intros i; destruct (ord_eq_dec i ord0) as [-> | Hi].
 rewrite ifF; [| destruct (pselect _)]; easy.
@@ -2490,8 +2493,10 @@ Lemma lenPF_ind_r_in :
   forall {n} {P : 'I_n.+1 -> Prop},
     P ord_max -> lenPF P = lenPF (fun i => P (widen_S i)) + 1.
 Proof.
-move=> n P /asboolP HP; unfold lenPF; rewrite (cardD1x HP) addnC; f_equal.
-apply sym_eq, (bijS_eq_card widen_S), injS_surjS_bijS.
+intros n P; destruct n as [|n];
+    [rewrite ord1; intros HP; rewrite (lenPF1_in HP) lenPF_nil add0n; easy |].
+move=> /asboolP HP; unfold lenPF; rewrite (cardD1x HP) addnC; f_equal.
+apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty).
 (* *)
 apply funS_correct; intro; destruct (pselect _); [| easy].
 intros _; apply /andP; split;
@@ -2518,7 +2523,9 @@ Lemma lenPF_ind_r_out :
   forall {n} {P : 'I_n.+1 -> Prop},
     ~ P ord_max -> lenPF P = lenPF (fun i => P (widen_S i)).
 Proof.
-intros; apply sym_eq, (bijS_eq_card widen_S), injS_surjS_bijS;
+intros n P HP; destruct n as [|n];
+    [rewrite ord1 in HP; rewrite (lenPF1_out HP) lenPF_nil; easy |].
+apply sym_eq, (bijS_eq_card widen_S), (injS_surjS_bijS I_S_is_nonempty);
     [apply funS_correct; easy | move=>> _ _; apply widen_ord_inj |].
 intros i; destruct (ord_eq_dec i ord_max) as [-> | Hi].
 rewrite ifF; [| destruct (pselect _)]; easy.
@@ -2530,8 +2537,10 @@ Lemma lenPF_skip_in :
   forall {n} {P : 'I_n.+1 -> Prop} {i0},
     P i0 -> lenPF P = 1 + lenPF (fun i => P (skip_ord i0 i)).
 Proof.
-move=> n P i0 /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
-apply sym_eq, (bijS_eq_card (skip_ord i0)), injS_surjS_bijS.
+intros n P i0; destruct n as [|n];
+    [rewrite ord1; intros HP; rewrite (lenPF1_in HP) lenPF_nil addn0; easy |].
+move=> /asboolP HP; unfold lenPF; rewrite (cardD1x HP); f_equal.
+apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty).
 (* *)
 apply funS_correct; intro; destruct (pselect _); [| easy].
 intros _; apply /andP; split;
@@ -2548,8 +2557,9 @@ Lemma lenPF_skip_out :
   forall {n} {P : 'I_n.+1 -> Prop} {i0},
     ~ P i0 -> lenPF P = lenPF (fun i => P (skip_ord i0 i)).
 Proof.
-move=> n P i0 HP; unfold lenPF;
-    apply sym_eq, (bijS_eq_card (skip_ord i0)), injS_surjS_bijS;
+intros n P i0 HP; destruct n as [|n];
+    [rewrite ord1 in HP; rewrite (lenPF1_out HP) lenPF_nil; easy |].
+apply sym_eq, (bijS_eq_card (skip_ord i0)), (injS_surjS_bijS I_S_is_nonempty);
     [apply funS_correct; easy | move=>> _ _; apply skip_ord_inj |].
 intros i; destruct (ord_eq_dec i i0) as [-> | Hi].
 rewrite ifF; [| destruct (pselect _)]; easy.
@@ -2679,7 +2689,7 @@ Proof.
 intros n1 n2 Hn P1 P2 HP j1; subst; rewrite cast_ord_id; destruct n2 as [|n2].
 exfalso; destruct j1 as [j1 Hj1]; rewrite lenPF_nil in Hj1; easy.
 unfold filterP_ord; rewrite !(enum_val_nth ord0); repeat f_equal.
-apply fun_ext; intro; f_equal; apply propositional_extensionality.
+apply fun_ext; intro; f_equal; apply prop_ext.
 rewrite HP cast_ord_id; easy.
 Qed.
 
@@ -2692,7 +2702,7 @@ intros n P Q H j.
 assert (H' : forall i, P i <-> Q (cast_ord erefl i))
     by now intros; rewrite cast_ord_id.
 rewrite (filterP_ord_ext_gen H') cast_ord_id.
-repeat f_equal; apply proof_irrelevance.
+repeat f_equal; apply proof_irrel.
 Qed.
 
 Lemma filterP_cast_ord :
@@ -2704,7 +2714,7 @@ intros n1 n2 H P1 j1; subst.
 assert (H' : forall i1, P1 i1 <-> P1 (cast_ord erefl i1))
     by now intros; rewrite cast_ord_id.
 rewrite cast_ord_id (filterP_ord_ext H').
-repeat f_equal; apply proof_irrelevance.
+repeat f_equal; apply proof_irrel.
 Qed.
 
 Lemma filterP_ord_ind_l_in_0 :
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 618f3bba134f662d664a40758b95bb043c3346b0..ef9ffb5d994fc1523e1347de96c7f9ee6ecde350 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -397,7 +397,7 @@ intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg];
     apply: (Bijective _ Hg); intro; auto.
 Qed.
 
-Lemma bij_ex_uniq :
+Lemma bij_ex_uniq_equiv :
   forall (f : T1 -> T2), bijective f <-> forall x2, exists! x1, f x1 = x2.
 Proof.
 intros f; rewrite bij_equiv; split.
@@ -502,7 +502,7 @@ Context {g : T1 -> T2}.
 Hypothesis Hg : bijective g.
 
 Lemma f_inv_ext : same_fun f g -> f_inv Hf = f_inv Hg.
-Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrelevance. Qed.
+Proof. move=> /fun_ext_equiv H; subst; f_equal; apply proof_irrel. Qed.
 
 End Inverse_Facts2.
 
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index a421a89b036cc759ebd3a4f45cc04343e0d04f65..428b98e917608c5668f220d2f2d7a8860622e696 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -23,10 +23,27 @@ From Lebesgue Require Import Subset Subset_dec Function.
 From FEM Require Import logic_compl Function_compl.
 
 
-(** Support for restrictions of functions to subsets. *)
+(** Support for restrictions of functions to subsets.
 
+  Let 'f : T1 -> T2' for any types 'T1' and 'T2'.
+  Let 'P1' and 'P2' respectively be subsets of 'T1' and 'T2'.
 
-Section Function_sub_Def0.
+  'RgS P1 f' is the range of 'f' restricted to 'P1' (an alias for 'image f P1').
+  'funS P1 P2 f' states that 'f' is a total function from 'P1' to 'P2',
+    namely that 'RgS P1 f' is included in 'P2'.
+  'injS P1 f' states that 'f' is injective on 'P1'
+    (definition similar to injective).
+  'surjS P1 P2 f' states that 'f' is surjective from 'P1' onto 'P2'
+    (definition similar to surjective).
+  'canS P1 f g' states that 'g' cancels 'f' on 'P1', ie it is its left inverse.
+    (definition similar to cancel).
+  'bijS P1 P2 f' states that 'f' is bijective from 'P1' onto 'P2'
+    (definition similar to bijective).
+
+ *)
+
+
+Section Fun_sub_Def1.
 
 Context {T1 T2 : Type}.
 
@@ -35,35 +52,24 @@ Variable P2 : T2 -> Prop.
 
 Variable f : T1 -> T2.
 
-Definition RgS := image f P1.
-Definition RgS_gen := inter P2 RgS.
+Definition RgS : T2 -> Prop := image f P1.
+Definition RgS_gen : T2 -> Prop := inter P2 RgS.
 
-(* The range of function f on subset P1 is in subset P2.
- This property makes the restriction of f from subset P1 to subset P2
- a total function. *)
 Definition funS : Prop := incl RgS P2.
 
-(* The function f is injective on subset P1. *)
 Definition injS : Prop :=
   forall x1 x2, P1 x1 -> P1 x2 -> f x1 = f x2 -> x1 = x2.
 
-(* The function f is surjective from subset P1 onto subset P2. *)
 Definition surjS : Prop := forall x2, P2 x2 -> exists x1, P1 x1 /\ f x1 = x2.
 
-(* The function f is bijjective from subset P1 onto subset P2. *)
-Definition bijS : Prop :=
-  funS /\ (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2).
-
 Variable g : T2 -> T1.
 
-(* The function g cancels the function f on subset P1,
- ie it is the left inverse of function f on subset P1. *)
 Definition canS : Prop := forall x1, P1 x1 -> g (f x1) = x1.
 
-End Function_sub_Def0.
+End Fun_sub_Def1.
 
 
-Section Function_sub_Def1.
+Section Fun_sub_Def2.
 
 Context {T1 T2 : Type}.
 
@@ -71,15 +77,21 @@ Variable P1 : T1 -> Prop.
 Variable P2 : T2 -> Prop.
 
 Variable f : T1 -> T2.
-Variable g : T2 -> T1.
 
-Definition bijS_alt : Prop :=
+Definition bijS_spec (g : T2 -> T1) : Prop :=
   funS P1 P2 f /\ funS P2 P1 g /\ canS P1 f g /\ canS P2 g f.
 
-End Function_sub_Def1.
+Variant bijS : Prop := BijS : forall g : T2 -> T1, bijS_spec g -> bijS.
+
+Lemma bijS_ex : bijS <-> exists g, bijS_spec g.
+Proof.
+split; [intros [g Hg]; exists g; easy | intros [g Hg]; apply (BijS g Hg)].
+Qed.
+
+End Fun_sub_Def2.
 
 
-Section Function_sub_Facts0a.
+Section RgS_Facts1.
 
 Context {T1 T2 : Type}.
 
@@ -111,88 +123,10 @@ Lemma RgS_gen_ex :
     RgS_gen P1 P2 f x2 <-> P2 x2 /\ (exists x1, P1 x1 /\ f x1 = x2).
 Proof. intros; rewrite -RgS_ex; easy. Qed.
 
-Lemma funS_correct : (forall x1, P1 x1 -> P2 (f x1)) -> funS P1 P2 f.
-Proof. intros Hf _ [x Hx]; auto. Qed.
+End RgS_Facts1.
 
-Lemma funS_rev : funS P1 P2 f -> forall x1, P1 x1 -> P2 (f x1).
-Proof. intros Hf x1 Hx1; apply Hf; easy. Qed.
-
-Lemma funS_equiv : funS P1 P2 f <-> forall x1, P1 x1 -> P2 (f x1).
-Proof. split; [apply funS_rev | apply funS_correct]. Qed.
 
-Lemma surjS_correct : incl P2 (RgS P1 f) -> surjS P1 P2 f.
-Proof.
-intros Hf x2 Hx2; destruct (Hf x2 Hx2) as [x1 Hx1]; exists x1; easy.
-Qed.
-
-Lemma surjS_rev : surjS P1 P2 f -> RgS_gen P1 P2 f = P2.
-Proof.
-intros Hf; apply incl_antisym; intros x2 Hx2; [apply Hx2 |].
-destruct (Hf _ Hx2) as [x1 Hx1]; apply (RgS_gen_correct x1); easy.
-Qed.
-
-End Function_sub_Facts0a.
-
-
-Section Function_sub_Facts0b.
-
-Context {T1 T2 : Type}.
-
-Context {P1 : T1 -> Prop}.
-Context {P2 : T2 -> Prop}.
-
-Context {f : T1 -> T2}.
-
-Lemma funS_id : funS P1 P1 id.
-Proof. apply funS_equiv; easy. Qed.
-
-Lemma surjS_equiv : surjS P1 P2 f <-> RgS_gen P1 P2 f = P2.
-Proof.
-split; [apply surjS_rev |].
-intros Hf; rewrite -Hf; apply surjS_correct, inter_lb_r.
-Qed.
-
-End Function_sub_Facts0b.
-
-
-Section Function_sub_Facts0c.
-
-Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
-
-Context {P1 : T1 -> Prop}.
-Context {P2 : T2 -> Prop}.
-
-Context {f : T1 -> T2}.
-
-Lemma bijS_ex : bijS P1 P2 f <-> (exists g, bijS_alt P1 P2 f g).
-Proof.
-split.
-(* *)
-intros [Hfa Hfb].
-destruct (choice (fun x2 x1 => P2 x2 -> P1 x1 /\ f x1 = x2)) as [g Hg].
-  intros x2; destruct (in_dec P2 x2) as [Hx2 | Hx2].
-  destruct (Hfb x2 Hx2) as [x1 [Hx1a Hx1b]]; exists x1; easy.
-  destruct HT1 as [x1]; exists x1; easy.
-exists g; repeat split; [easy |..].
-intros _ [x2 Hx2]; apply Hg; easy.
-2: intros x2 Hx2; apply Hg; easy.
-assert (Hfc : injS P1 f).
-  intros x1 x2 Hx1 Hx2 Hx.
-  destruct (Hfb (f x1)) as [y1 [Hy1a Hy1b]]; [apply Hfa; easy |].
-  rewrite -(Hy1b x1); [apply Hy1b |]; easy.
-rewrite funS_equiv in Hfa.
-intros x1 Hx1; apply Hfc; try apply Hg; auto.
-(* *)
-move=> [g [Hf [/funS_equiv Hg [Hfl Hfr]]]]; split; try easy.
-intros x2 Hx2; exists (g x2); repeat split; auto.
-move=> x1 [Hx1a <-]; auto.
-Qed.
-
-End Function_sub_Facts0c.
-
-
-Section Function_sub_Facts1.
+Section RgS_Facts2.
 
 Context {T1 T2 T3 : Type}.
 
@@ -251,6 +185,52 @@ Qed.
 Lemma Rg_comp_alt : Rg (g \o f) = RgS (Rg f) g.
 Proof. apply Rg_comp. Qed.
 
+End RgS_Facts2.
+
+
+Section FunS_Facts1.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
+Lemma funS_correct : (forall x1, P1 x1 -> P2 (f x1)) -> funS P1 P2 f.
+Proof. intros Hf _ [x Hx]; auto. Qed.
+
+Lemma funS_rev : funS P1 P2 f -> forall x1, P1 x1 -> P2 (f x1).
+Proof. intros Hf x1 Hx1; apply Hf; easy. Qed.
+
+Lemma funS_equiv : funS P1 P2 f <-> forall x1, P1 x1 -> P2 (f x1).
+Proof. split; [apply funS_rev | apply funS_correct]. Qed.
+
+End FunS_Facts1.
+
+
+Section FunS_Facts2.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Lemma funS_id : funS P1 P1 id.
+Proof. apply funS_equiv; easy. Qed.
+
+End FunS_Facts2.
+
+
+Section FunS_Facts3.
+
+Context {T1 T2 : Type}.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
 Lemma funS_full_l :
   forall P2 (f : T1 -> T2), incl (Rg f) P2 -> funS fullset P2 f.
 Proof. easy. Qed.
@@ -261,98 +241,84 @@ Proof. easy. Qed.
 Lemma funS_full : forall (f : T1 -> T2), funS fullset fullset f.
 Proof. easy. Qed.
 
-Lemma funS_comp :
-  forall P2 P3 (f : T1 -> T2) (g : T2 -> T3),
-    funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
+End FunS_Facts3.
+
+
+Section FunS_Facts4.
+
+Context {T1 T2 T3 : Type}.
+
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
+
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
+
+Lemma funS_comp_compat : funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
 Proof.
-intros P2' P3' f' g' Hf' Hg' x3 [x1 Hx1]; rewrite comp_correct;
-    apply Hg', (RgS_correct (f' x1));
-    [apply Hf'; apply (RgS_correct x1) |]; easy.
+move=> /funS_equiv Hf /funS_equiv Hg _ [x1 Hx1]; apply Hg, Hf; easy.
 Qed.
 
-Lemma surjS_equiv_alt : surjS P1 P2 f <-> incl P2 (RgS P1 f).
-Proof. rewrite surjS_equiv; apply RgS_gen_full_equiv. Qed.
-
-End Function_sub_Facts1.
+End FunS_Facts4.
 
 
-Section Function_sub_Facts2a.
+Section InjS_Facts1.
 
 Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
 
-Context {P1 : T1 -> Prop}.
-Context {P2 : T2 -> Prop}.
+Variable f : T1 -> T2.
 
-Context {f : T1 -> T2}.
+Lemma inj_S_equiv : injective f <-> injS fullset f.
+Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
 
-Lemma bijS_funS : bijS P1 P2 f -> funS P1 P2 f.
-Proof. unfold bijS; easy. Qed.
+End InjS_Facts1.
 
-Lemma bijS_injS : forall P2 {f : T1 -> T2}, bijS P1 P2 f -> injS P1 f.
-Proof.
-move=>> /(bijS_ex HT1) [g [Hf [_ [Hg _]]]] x1 y1 Hx1 Hy1 H1;
-    rewrite -(Hg x1)// -(Hg y1)// H1; easy.
-Qed.
 
-Lemma bijS_surjS : bijS P1 P2 f -> surjS P1 P2 f.
-Proof.
-move=> /(bijS_ex HT1) [g [_ [/funS_equiv Hg [_ Hfr]]]] x2 Hx2;
-    exists (g x2); auto.
-Qed.
+Section InjS_Facts2.
 
-Lemma injS_surjS_bijS :
-  funS P1 P2 f -> injS P1 f -> surjS P1 P2 f -> bijS P1 P2 f.
+Context {T1 T2 T3 : Type}.
+
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
+
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
+
+Lemma injS_comp_compat :
+  funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
 Proof.
-intros Hf1a Hf1b Hf2; split; [easy |].
-intros x2 Hx2; destruct (Hf2 _ Hx2) as [x1 Hx1]; exists x1; split; [easy |].
-intros y1 Hy1; apply Hf1b; [..| apply trans_eq with x2]; easy.
+intros Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
 Qed.
 
-Lemma bijS_equiv : bijS P1 P2 f <-> funS P1 P2 f /\ injS P1 f /\ surjS P1 P2 f.
+Lemma injS_comp_reg : injS P1 (g \o f) -> injS P1 f.
 Proof.
-split; intros Hf; [split; [apply bijS_funS; easy |] |].
-split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
-apply injS_surjS_bijS; easy.
+intros H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
 Qed.
 
-End Function_sub_Facts2a.
+End InjS_Facts2.
 
 
-Section Function_sub_Facts2b.
+Section SurjS_Facts1.
 
 Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
 
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
-Lemma surjS_RgS : forall P1 (f : T1 -> T2), surjS P1 (RgS P1 f) f.
-Proof. intros; apply surjS_correct; easy. Qed.
-
-Lemma bijS_RgS_equiv : bijS P1 (RgS P1 f) f <-> injS P1 f.
+Lemma surjS_correct : incl P2 (RgS P1 f) -> surjS P1 P2 f.
 Proof.
-rewrite bijS_equiv//; split; [easy |].
-intros; repeat split; [| | apply surjS_RgS]; easy.
+intros Hf x2 Hx2; destruct (Hf x2 Hx2) as [x1 Hx1]; exists x1; easy.
 Qed.
 
-End Function_sub_Facts2b.
-
-
-Section Function_sub_Facts3.
-
-Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
-
-Variable P1 : T1 -> Prop.
-Variable P2 : T2 -> Prop.
-
-Variable f : T1 -> T2.
-
-Lemma inj_S_equiv : injective f <-> injS fullset f.
-Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
+Lemma surjS_rev : surjS P1 P2 f -> RgS_gen P1 P2 f = P2.
+Proof.
+intros Hf; apply incl_antisym; intros x2 Hx2; [apply Hx2 |].
+destruct (Hf _ Hx2) as [x1 Hx1]; apply (RgS_gen_correct x1); easy.
+Qed.
 
 Lemma surj_S_equiv : surjective f <-> surjS fullset fullset f.
 Proof.
@@ -361,46 +327,62 @@ intros x2 _; destruct (Hf x2) as [x1 Hx1]; exists x1; easy.
 intros x2; destruct (Hf x2) as [x1 Hx1]; [| exists x1]; easy.
 Qed.
 
-Lemma bij_S_equiv : bijective f <-> bijS fullset fullset f.
-Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed.
+End SurjS_Facts1.
 
-End Function_sub_Facts3.
 
-
-Section Function_sub_Facts4.
+Section SurjS_Facts2.
 
 Context {T1 T2 : Type}.
-Hypothesis HT1 : inhabited T1.
-Hypothesis HT2 : inhabited T2.
 
 Context {P1 : T1 -> Prop}.
 Context {P2 : T2 -> Prop}.
 
 Context {f : T1 -> T2}.
 
-Lemma f_invS_EX : bijS P1 P2 f -> { f1 : T2 -> T1 | bijS_alt P1 P2 f f1 }.
-Proof. intros Hf; apply ex_EX; apply bijS_ex; easy. Qed.
+Lemma surjS_equiv : surjS P1 P2 f <-> RgS_gen P1 P2 f = P2.
+Proof.
+split; [apply surjS_rev |].
+intros Hf; rewrite -Hf; apply surjS_correct, inter_lb_r.
+Qed.
 
-Definition f_invS (Hf : bijS P1 P2 f) := proj1_sig (f_invS_EX Hf).
+Lemma surjS_equiv_alt : surjS P1 P2 f <-> incl P2 (RgS P1 f).
+Proof. rewrite surjS_equiv; apply RgS_gen_full_equiv. Qed.
 
-Hypothesis Hf : bijS P1 P2 f.
+Lemma surjS_RgS : forall P1 (f : T1 -> T2), surjS P1 (RgS P1 f) f.
+Proof. intros; apply surjS_correct; easy. Qed.
 
-Lemma f_invS_funS_l : funS P1 P2 f.
-Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
+End SurjS_Facts2.
+
+
+Section SurjS_Facts3.
+
+Context {T1 T2 T3 : Type}.
+
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
 
-Lemma f_invS_funS_r : funS P2 P1 (f_invS Hf).
-Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
 
-Lemma f_invS_canS_l : canS P2 (f_invS Hf) f.
-Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
+Lemma surjS_comp_compat :
+  surjS P1 P2 f -> surjS P2 P3 g -> surjS P1 P3 (g \o f).
+Proof.
+intros Hf Hg x3 Hx3;
+    destruct (Hg _ Hx3) as [x2 [Hx2a Hx2b]], (Hf _ Hx2a) as [x1 [Hx1a Hx1b]].
+exists x1; split; [| rewrite comp_correct Hx1b]; easy.
+Qed.
 
-Lemma f_invS_canS_r : canS P1 f (f_invS Hf).
-Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
+Lemma surjS_comp_reg : funS P1 P2 f -> surjS P1 P3 (g \o f) -> surjS P2 P3 g.
+Proof.
+intros Hf H x3 Hx3; destruct (H _ Hx3) as [x1 [Hx1a Hx1b]].
+exists (f x1); split; [apply Hf |]; easy.
+Qed.
 
-End Function_sub_Facts4.
+End SurjS_Facts3.
 
 
-Section Function_sub_Facts5a.
+Section CanS_Facts1.
 
 Context {T1 T2 T3 : Type}.
 
@@ -411,49 +393,127 @@ Variable P3 : T3 -> Prop.
 Variable f : T1 -> T2.
 Variable g : T2 -> T3.
 
-Lemma funS_comp_compat : funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
+Lemma canS_comp_compat :
+  forall {f1 g1},
+    funS P1 P2 f -> canS P1 f f1 -> canS P2 g g1 ->
+    canS P1 (g \o f) (f1 \o g1).
 Proof.
-move=> /funS_equiv Hf /funS_equiv Hg _ [x1 Hx1]; apply Hg, Hf; easy.
+move=>> /funS_equiv H1 H2 H3 x1 Hx1; rewrite -> !comp_correct, H3, H2; auto.
 Qed.
 
-Lemma injS_comp_compat :
-  funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
+End CanS_Facts1.
+
+
+Section BijS_Facts1.
+
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
+Lemma bijS_ex_uniq :
+  bijS P1 P2 f ->
+  funS P1 P2 f /\ (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2).
 Proof.
-intros Hf0 Hf Hg x1 y1 Hx1 Hy1 H1; apply Hf, Hg; try apply Hf0; easy.
+clear HT1; move=> [g [H1 [/funS_equiv H2 [H3 H4]]]]; split; [easy |].
+intros x2 Hx2; exists (g x2); repeat split; auto.
+move=> x1 [Hx1 <-]; auto.
 Qed.
 
-Lemma injS_comp_reg : injS P1 (g \o f) -> injS P1 f.
+Lemma bijS_ex_uniq_rev :
+  funS P1 P2 f -> (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2) ->
+  bijS P1 P2 f.
 Proof.
-intros H x1 y1 Hx1 Hy1 H1; apply H; try rewrite comp_correct H1; easy.
+intros H1 H2.
+destruct (choice (fun x2 x1 => P2 x2 -> P1 x1 /\ f x1 = x2)) as [g Hg].
+  intros x2; destruct (in_dec P2 x2) as [Hx2 | Hx2].
+  destruct (H2 x2 Hx2) as [x1 [Hx1a Hx1b]]; exists x1; easy.
+  destruct HT1 as [x1]; exists x1; easy.
+apply (BijS _ _ _ g); repeat split; [easy |..].
+intros _ [x2 Hx2]; apply Hg; easy.
+2: intros x2 Hx2; apply Hg; easy.
+assert (H3 : injS P1 f).
+  intros x1 x2 Hx1 Hx2 Hx.
+  destruct (H2 (f x1)) as [y1 [Hy1a Hy1b]]; [apply H1; easy |].
+  rewrite -(Hy1b x1); [apply Hy1b |]; easy.
+rewrite funS_equiv in H1.
+intros x1 Hx1; apply H3; try apply Hg; auto.
 Qed.
 
-Lemma surjS_comp_compat :
-  surjS P1 P2 f -> surjS P2 P3 g -> surjS P1 P3 (g \o f).
+Lemma bijS_ex_uniq_equiv :
+  bijS P1 P2 f <->
+  funS P1 P2 f /\ (forall x2, P2 x2 -> exists! x1, P1 x1 /\ f x1 = x2).
+Proof. split; [apply bijS_ex_uniq | intros; apply bijS_ex_uniq_rev; easy]. Qed.
+
+End BijS_Facts1.
+
+
+Section BijS_Facts2.
+
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
+Lemma bijS_funS : bijS P1 P2 f -> funS P1 P2 f.
+Proof. intros [g Hg]; apply Hg. Qed.
+
+Lemma bijS_injS : forall P2 {f : T1 -> T2}, bijS P1 P2 f -> injS P1 f.
 Proof.
-intros Hf Hg x3 Hx3;
-    destruct (Hg _ Hx3) as [x2 [Hx2a Hx2b]], (Hf _ Hx2a) as [x1 [Hx1a Hx1b]].
-exists x1; split; [| rewrite comp_correct Hx1b]; easy.
+move=>> [g [Hf [_ [Hg _]]]] x1 y1 Hx1 Hy1 H1;
+    rewrite -(Hg x1)// -(Hg y1)// H1; easy.
 Qed.
 
-Lemma surjS_comp_reg : funS P1 P2 f -> surjS P1 P3 (g \o f) -> surjS P2 P3 g.
+Lemma bijS_surjS : bijS P1 P2 f -> surjS P1 P2 f.
+Proof. move=> [g [_ [/funS_equiv Hg [_ Hf]]]] x2 Hx2; exists (g x2); auto. Qed.
+
+Lemma injS_surjS_bijS :
+  funS P1 P2 f -> injS P1 f -> surjS P1 P2 f -> bijS P1 P2 f.
 Proof.
-intros Hf H x3 Hx3; destruct (H _ Hx3) as [x1 [Hx1a Hx1b]].
-exists (f x1); split; [apply Hf |]; easy.
+move=> H1 H2 H3; apply bijS_ex_uniq_rev; [easy.. |].
+intros x2 Hx2; destruct (H3 _ Hx2) as [x1 Hx1]; exists x1; split; [easy |].
+intros y1 Hy1; apply H2; [..| apply trans_eq with x2]; easy.
 Qed.
 
-Lemma canS_comp_compat :
-  forall {fm1 gm1},
-    funS P1 P2 f -> canS P1 f fm1 -> canS P2 g gm1 ->
-    canS P1 (g \o f) (fm1 \o gm1).
+Lemma bijS_equiv : bijS P1 P2 f <-> funS P1 P2 f /\ injS P1 f /\ surjS P1 P2 f.
 Proof.
-move=>> /funS_equiv Hf Hfm1 Hgm1 x1 Hx1.
-rewrite -> !comp_correct, Hgm1, Hfm1; auto.
+split; intros Hf; [split; [apply bijS_funS; easy |] |].
+split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
+apply injS_surjS_bijS; easy.
+Qed.
+
+End BijS_Facts2.
+
+
+Section BijS_Facts3.
+
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+
+Lemma bijS_RgS_equiv : bijS P1 (RgS P1 f) f <-> injS P1 f.
+Proof.
+rewrite bijS_equiv//; split; [easy |].
+intros; repeat split; [| | apply surjS_RgS]; easy.
 Qed.
 
-End Function_sub_Facts5a.
+Lemma bij_S_equiv : bijective f <-> bijS fullset fullset f.
+Proof. rewrite bij_equiv bijS_equiv// inj_S_equiv surj_S_equiv; easy. Qed.
+
+End BijS_Facts3.
 
 
-Section Function_sub_Facts5b.
+Section BijS_Facts4.
 
 Context {T1 T2 T3 : Type}.
 Hypothesis HT1 : inhabited T1.
@@ -466,34 +526,61 @@ Variable P3 : T3 -> Prop.
 Variable f : T1 -> T2.
 Variable g : T2 -> T3.
 
-Lemma bijS_alt_comp_compat :
-  forall fm1 gm1,
-    bijS_alt P1 P2 f fm1 -> bijS_alt P2 P3 g gm1 ->
-    bijS_alt P1 P3 (g \o f) (fm1 \o gm1).
+Lemma bijS_spec_comp_compat :
+  forall f1 g1,
+    bijS_spec P1 P2 f f1 -> bijS_spec P2 P3 g g1 ->
+    bijS_spec P1 P3 (g \o f) (f1 \o g1).
 Proof.
-intros fm1 gm1 [Hf1 [Hf2 [Hf3 Hf4]]] [Hg1 [Hg2 [Hg3 Hg4]]]; repeat split.
+intros f1 g1 [Hf1 [Hf2 [Hf3 Hf4]]] [Hg1 [Hg2 [Hg3 Hg4]]]; repeat split.
 1,2: apply funS_comp_compat with P2; easy.
 1,2: apply canS_comp_compat with P2; easy.
 Qed.
 
 Lemma bijS_comp_compat : bijS P1 P2 f -> bijS P2 P3 g -> bijS P1 P3 (g \o f).
 Proof.
-move=> /(bijS_ex HT1) [fm1 Hfm1] /(bijS_ex HT2) [gm1 Hgm1].
-apply (bijS_ex HT1); exists (fm1 \o gm1).
-apply bijS_alt_comp_compat; easy.
+intros [f1 Hf] [g1 Hg]; exists (f1 \o g1); apply bijS_spec_comp_compat; easy.
 Qed.
 
 Lemma bijS_comp_injS : funS P1 P2 f -> bijS P1 P3 (g \o f) -> injS P1 f.
 Proof.
-intros H0 H1; move: (proj1 (bijS_equiv HT1) H1) => [_ [H2 _]].
+intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [H3 _]].
 apply injS_comp_reg with g; easy.
 Qed.
 
 Lemma bijS_comp_surjS :
   funS P1 P2 f -> bijS P1 P3 (g \o f) -> surjS P2 P3 g.
 Proof.
-intros H0 H1; move: (proj1 (bijS_equiv HT1) H1) => [_ [_ H2]].
+intros H1 H2; move: (proj1 (bijS_equiv HT1) H2) => [_ [_ H3]].
 apply surjS_comp_reg with P1 f; easy.
 Qed.
 
-End Function_sub_Facts5b.
+End BijS_Facts4.
+
+
+Section F_invS_Def.
+
+Context {T1 T2 : Type}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+
+Context {f : T1 -> T2}.
+Hypothesis Hf : bijS P1 P2 f.
+
+Lemma f_invS_EX : { g : T2 -> T1 | bijS_spec P1 P2 f g }.
+Proof. apply ex_EX; induction Hf as [g [H1 [H2 [H3 H4]]]]; exists g; easy. Qed.
+
+Definition f_invS : T2 -> T1 := proj1_sig f_invS_EX.
+
+Lemma f_invS_funS_l : funS P1 P2 f.
+Proof. apply (proj2_sig f_invS_EX). Qed.
+
+Lemma f_invS_funS_r : funS P2 P1 f_invS.
+Proof. apply (proj2_sig f_invS_EX). Qed.
+
+Lemma f_invS_canS_l : canS P2 f_invS f.
+Proof. apply (proj2_sig f_invS_EX). Qed.
+
+Lemma f_invS_canS_r : canS P1 f f_invS.
+Proof. apply (proj2_sig f_invS_EX). Qed.
+
+End F_invS_Def.
diff --git a/FEM/Compl/logic_compl.v b/FEM/Compl/logic_compl.v
index 466f3c6f55c6c022e08826f1d639c12735ba6075..50dad16015bb1895c358d0d18c68234623f5b237 100644
--- a/FEM/Compl/logic_compl.v
+++ b/FEM/Compl/logic_compl.v
@@ -14,8 +14,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(* We need classical logic, and a constructive form of indefinite description. *)
-From Coq Require Import Classical IndefiniteDescription.
+(* We need propositional extensionality, classical logic, and a constructive
+ form of indefinite description. *)
+From Coq Require Import PropExtensionality Classical IndefiniteDescription.
 
 
 (** Additional definitions and results about classical logic.
@@ -23,6 +24,9 @@ From Coq Require Import Classical IndefiniteDescription.
   'neq' is the "not eq" binary relation on any type.
   'br_not R' is the negation of any binary relation 'R' on any type.
 
+  'prop_ext' is an alias for 'propositional_extensionality'.
+  'proof_irrel' is an alias for 'proof_irrelevance'.
+
   Provide equivalence results to enable the use of the rewrite tactic.
   All names use the "_equiv" prefix. These are for:
   - all propositional connectives, possibly in various configurations;
@@ -55,6 +59,12 @@ Proof. tauto. Qed.
 Lemma NNPP_equiv : forall (P : Prop), ~ ~ P <-> P.
 Proof. intros; tauto. Qed.
 
+Lemma prop_ext : forall (P Q : Prop), P <-> Q -> P = Q.
+Proof. exact propositional_extensionality. Qed.
+
+Lemma proof_irrel : forall (H : Prop) (P Q : H), P = Q.
+Proof. exact proof_irrelevance. Qed.
+
 End Classical_propositional_Facts1.
 
 
@@ -163,7 +173,7 @@ Lemma eq_sym_refl : eq_sym (@eq_refl _ x) = @eq_refl _ x.
 Proof. easy. Qed.
 
 Lemma neq_sym_invol : forall (H : x <> y), not_eq_sym (not_eq_sym H) = H.
-Proof. intros; apply proof_irrelevance. Qed.
+Proof. intros; apply proof_irrel. Qed.
 
 End Classical_propositional_Facts5.
 
diff --git a/FEM/FE.v b/FEM/FE.v
index 55ad43e33beab108d2b7ca87499aca0a0f54c3de..b46027fdaa78afa1590a3daff6e410a03ae5681a 100644
--- a/FEM/FE.v
+++ b/FEM/FE.v
@@ -62,7 +62,7 @@ Definition is_unisolvent : (FRd d-> 'R^n) -> Prop :=
 Lemma is_unisolvent_bijS : forall sigma : FRd d-> 'R^n,
    is_unisolvent sigma  <-> bijS P fullset sigma.
 Proof.
-intros sigma; split.
+intros sigma; rewrite (bijS_ex_uniq_equiv inhabited_fct_r); split.
 (* => *)
 intros H; split; try easy.
 intros y Hy; destruct (H y) as [p Hp].
@@ -126,7 +126,7 @@ Lemma is_unisolvent_is_free :
      is_unisolvent sigma -> is_free (scatter sigma).
 Proof.
 intros sigma Hs1 Hs2.
-apply is_unisolvent_bijS in Hs2.
+apply is_unisolvent_bijS, bijS_ex_uniq in Hs2.
 destruct Hs2 as (Hs2,Hs3).
 intros L HL.
 apply extF; intros k.
@@ -156,7 +156,7 @@ Lemma is_unisolvent_ext : forall (sigma1 sigma2 : FRd d -> 'R^n),
     is_unisolvent d n P2 P2_compatible_finite sigma2.
 Proof.
 intros; subst.
-rewrite (proof_irrelevance _  P2_compatible_finite P1_compatible_finite); easy.
+rewrite (proof_irrel _  P2_compatible_finite P1_compatible_finite); easy.
 Qed.
 
 End is_unisolvent_Fact.
diff --git a/FEM/FE_LagP.v b/FEM/FE_LagP.v
index b9e63f8489ed2904228e098f0feae236cde4a418..4cefe8a5afac2a41001520a75a13260b1673a874 100644
--- a/FEM/FE_LagP.v
+++ b/FEM/FE_LagP.v
@@ -457,7 +457,7 @@ Lemma Phi_bijS :
     bijS fullset (face_hyp_0 d1.+1 vtx_cur) (Phi d1 vtx_cur).
 Proof.
 intros d1 vtx_cur Hvtx.
-apply injS_surjS_bijS.
+apply (injS_surjS_bijS inhabited_fct_ms).
 apply Phi_in_face_hyp_0; try easy.
 rewrite (injS_aff_lin_equiv_alt invertible_2 compatible_as_fullset
   (Phi_is_affine_mapping d1 vtx_cur) 0%M); try easy.
@@ -522,11 +522,11 @@ assert (Y1 : forall x : 'R^dL.+1,
   face_hyp_0 dL.+1 vtx_cur x -> p x = 0).
 intros x Hx.
 assert (Y2 : forall y : 'R^dL.+1,  face_hyp_0 dL.+1 vtx_cur y ->
-  p y = p0' (f_invS inhabited_m (Phi_bijS dL vtx_cur Hvtx) y)).
+  p y = p0' (f_invS (Phi_bijS dL vtx_cur Hvtx) y)).
 unfold p0'.
 intros y Hy.
 unfold compose.
-rewrite (f_invS_canS_l inhabited_m (Phi_bijS dL vtx_cur Hvtx)); try easy.
+rewrite (f_invS_canS_l (Phi_bijS dL vtx_cur Hvtx)); try easy.
 unfold funS.
 rewrite Y2; try easy.
 apply val_eq in IH1.
diff --git a/FEM/FE_simplex.v b/FEM/FE_simplex.v
index 47dd1f7eef0855bef40297857ff027e5085b57aa..cf904133ff1bde947854ce3dbe308284595ae017 100644
--- a/FEM/FE_simplex.v
+++ b/FEM/FE_simplex.v
@@ -111,7 +111,7 @@ Proof.
 (* simplifier la preuve *)
 apply fun_ext.
 intros x; unfold K_geom_ref, K_geom; unfold vtx_ref.
-apply propositional_extensionality; split.
+apply prop_ext; split.
 eapply convex_envelop_cast with (H:=sym_eq nnvtx_eq_S_dd); intros i; f_equal;
    apply ord_inj; easy.
 eapply convex_envelop_cast with (H:=nnvtx_eq_S_dd); intros i; f_equal;
@@ -320,7 +320,7 @@ apply fun_ext.
 intros x; unfold K_geom_cur, K_geom.
 replace (vtx FE_cur) with (fun i => vtx_cur (ord_nvtx_Sd i)).
 2: apply fun_ext; unfold FE_cur; simpl; easy.
-apply propositional_extensionality; split.
+apply prop_ext; split.
 eapply convex_envelop_cast with (H:=H).
 intros i; f_equal; apply ord_inj; easy.
 apply sym_eq in H.
@@ -334,7 +334,7 @@ Proof.
 rewrite image_eq.
 unfold image_ex.
 apply fun_ext; intros x_cur.
-apply propositional_extensionality.
+apply prop_ext.
 split.
 (* *)
 intros [x_ref [Hx1 Hx2]].
@@ -354,7 +354,7 @@ Proof.
 rewrite image_eq.
 unfold image_ex.
 apply fun_ext; intros x_ref.
-apply propositional_extensionality.
+apply prop_ext.
 split.
 (* *)
 intros [x_cur [Hx1 Hx2]].
@@ -368,8 +368,8 @@ apply P_approx_cur_correct; easy.
 apply cur_to_ref_comp; easy. 
 Qed.
 
-Lemma cur_to_ref_bijS_alt :
-  bijS_alt P_approx_ref P_approx_cur ref_to_cur cur_to_ref.
+Lemma cur_to_ref_bijS_spec :
+  bijS_spec P_approx_ref P_approx_cur ref_to_cur cur_to_ref.
 Proof.
 repeat split.
 intros _ [x_ref H1]; apply P_approx_cur_correct; easy.
diff --git a/FEM/multi_index.v b/FEM/multi_index.v
index 7186854cf7acd615be90ca9a0b3da49e54af8263..ac1df92bbba17d2ee1724f491179f1f9adb1892a 100644
--- a/FEM/multi_index.v
+++ b/FEM/multi_index.v
@@ -47,7 +47,7 @@ Lemma MOn_correct1 : forall x y : 'nat^1, MOn x y = (x ord0 < y ord0)%coq_nat.
 Proof.
 intros x y; simpl; rewrite 2!sum_1.
 assert (H : forall P Q, (P \/ Q /\ False) = P)
-    by (intros; apply propositional_extensionality; tauto).
+    by (intros; apply prop_ext; tauto).
 apply H.
 Qed.
 
@@ -76,7 +76,7 @@ Proof.
 intros x y; simpl; rewrite !sum_2 !sum_1 !castF_refl !skipF_2l0.
 unfold MO2; f_equal.
 assert (H : forall P Q R, (P /\ (Q \/ R /\ False)) = (P /\ Q))
-    by (intros; apply propositional_extensionality; tauto).
+    by (intros; apply prop_ext; tauto).
 apply H.
 Qed.
 *)
diff --git a/FEM/poly_Lagrange.v b/FEM/poly_Lagrange.v
index 255ebc375385c5bf5556b1cf743a9d1ca56e39ea..fd61ac9706a02be8f22d9889902dc3e723fc13c9 100644
--- a/FEM/poly_Lagrange.v
+++ b/FEM/poly_Lagrange.v
@@ -1404,7 +1404,7 @@ Proof.
 rewrite image_eq.
 unfold image_ex.
 apply fun_ext; intros x_cur.
-apply propositional_extensionality.
+apply prop_ext.
 split.
 (* *)
 intros [x_ref [Hx1 Hx2]].
@@ -1424,7 +1424,7 @@ Proof.
 rewrite image_eq.
 unfold image_ex.
 apply fun_ext; intros x_ref.
-apply propositional_extensionality.
+apply prop_ext.
 split.
 (* *)
 intros [x_cur [Hx1 Hx2]].
@@ -1438,8 +1438,8 @@ apply K_geom_cur_correct; easy.
 apply T_geom_inv_comp; easy. 
 Qed.
 
-Lemma T_geom_bijS_alt :
-  bijS_alt K_geom_cur K_geom_ref T_geom_inv T_geom.
+Lemma T_geom_bijS_spec :
+  bijS_spec K_geom_cur K_geom_ref T_geom_inv T_geom.
 Proof.
 split.
 intros _ [x_cur H]; apply K_geom_ref_correct; easy.
@@ -1462,8 +1462,8 @@ intros x_cur; rewrite <- T_geom_comp; easy.
 apply (Bijective H1 H2).
 Qed.
 
-Lemma T_geom_inv_bijS_alt :
-  bijS_alt K_geom_ref K_geom_cur T_geom T_geom_inv.
+Lemma T_geom_inv_bijS_spec :
+  bijS_spec K_geom_ref K_geom_cur T_geom T_geom_inv.
 Proof.
 split.
 intros _ [x_ref H]; apply K_geom_cur_correct; easy.
@@ -1481,9 +1481,8 @@ Lemma T_geom_inv_bijS :
   bijS K_geom_cur K_geom_ref T_geom_inv.
 Proof.
 apply bijS_ex.
-apply inhabited_ms.
 exists T_geom.
-apply T_geom_bijS_alt.
+apply T_geom_bijS_spec.
 Qed.
 
 Lemma T_geom_inv_eq :