diff --git a/FEM/Algebra/Sub_struct.v b/FEM/Algebra/Sub_struct.v
index 93362edaddb0b7e043260813e722c762ec5073dc..2533756b499f01e4a4ec6c6bdf1dae466928ac20 100644
--- a/FEM/Algebra/Sub_struct.v
+++ b/FEM/Algebra/Sub_struct.v
@@ -2646,7 +2646,7 @@ Proof.
 intros PE HK [O HE].
 destruct (empty_dec PE) as [HPE | HPE].
 apply compatible_as_empty; easy.
-rewrite (unit_nonempty_subset_is_singleton PE _ HE HPE).
+rewrite (unit_subset_is_singleton PE HE HPE).
 apply compatible_as_singleton.
 Qed.
 
diff --git a/FEM/Compl/Compl.v b/FEM/Compl/Compl.v
index 3115ea8ddf3eaa2577721556e437a33e175c808b..30238f5ce6f1956361beb5e00010f78a162c1257 100644
--- a/FEM/Compl/Compl.v
+++ b/FEM/Compl/Compl.v
@@ -14,5 +14,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
+(** Export of complements. *)
+
 From FEM.Compl Require Export logic_compl.
 From FEM.Compl Require Export Subset_compl Function_compl Function_sub.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index fc25c10da17b4bb41ff9392b48f15a87ea2d5bce..0bc450afd09a6cf7f60b38a60b2a0ca2c5256c92 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -14,101 +14,210 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import ClassicalEpsilon.
-From Coq Require Import Arith.
-From Coq Require Import ssreflect ssrfun ssrbool.
+(* We need non-unique choice. *)
+From Coq Require Import ClassicalChoice.
+From Coq Require Import ssreflect ssrfun.
 
-Set Warnings "-notation-overridden".
-From mathcomp Require Import ssrnat fintype.
-Set Warnings "notation-overridden".
-
-From Lebesgue Require Import nat_compl Subset Function.
+(* We need decidability of the belonging to a subset, and functional extensionality. *)
+From Lebesgue Require Import Subset Subset_dec Function.
 
+(* We need classical logic, and a constructive form of indefinite description. *)
 From FEM Require Import logic_compl.
 
 
-Section Function_Facts1.
+(** Additional definitions and results about functions.
+  This complements the file Lebesgue.Function, and results from mathcomp.
+
+  Additional support for functional extensionality.
+  Provide more results, including equivalence results to enable the use
+    of the rewrite tactic.
+
+  Support for functions from/to types that are inhabited or not.
+  'fun_from_empty' is the only function from an empty type to another type,
+    empty or not.
+  'fun_from_empty_is_inj' states that it is injective.
+  'fun_to_empty_is_empty' states that there is no function from a nonempty
+    type to an empty one.
+
+  Additional support for image/preimage.
+  'Rg f' is the range of a function f (an alias for 'image f fullset').
+
+  Additional support for the composition of functions.
+  'comp_inj_r' states the condition for composition to be injective wrt
+    its second (right) argument.
+
+  Additional support for injective/surjective/bijective functions.
+  'im_dec' is a decidability result stating that any element of the output type
+    of any function is either in its image/range or not.
+  '{inj,surj}_has_left_inv' states that injective (resp. surjective) functions
+    have a left (resp. right) inverse.
+
+  Support for the inverse of bijective functions.
+  'f_inv_EX' states the strong existence of the (left and right) inverse of
+    any bijective function.
+  'f_inv Hf' is the inverse of any function from any proof Hf of its bijectivity.
+  The inverse of any bijective function is unique and bijective.
+  Involutive functions are the bijective functions equal to their inverse.
+ *)
+
+
+Section Functional_extensionality_Facts.
+
+Context {T1 T2 : Type}.
+Variable f g : T1 -> T2.
+
+Lemma fun_ext_rev : f = g -> forall x1, f x1 = g x1.
+Proof. intros; subst; easy. Qed.
+
+Lemma fun_ext_equiv : f = g <-> forall x1, f x1 = g x1.
+Proof. split; [apply fun_ext_rev | apply fun_ext]. Qed.
+
+Lemma fun_ext_contra : f <> g -> exists x1, f x1 <> g x1.
+Proof. rewrite contra_not_l_equiv not_ex_not_all_equiv; apply fun_ext. Qed.
+
+Lemma fun_ext_contra_rev : (exists x1, f x1 <> g x1) -> f <> g.
+Proof. rewrite contra_not_r_equiv not_ex_not_all_equiv; apply fun_ext_rev. Qed.
+
+Lemma fun_ext_contra_equiv : f <> g <-> exists x1, f x1 <> g x1.
+Proof. split; [apply fun_ext_contra | apply fun_ext_contra_rev]. Qed.
 
-Context {U1 U2 : Type}.
+End Functional_extensionality_Facts.
 
-Lemma fun_to_nonempty_compat : inhabited U2 -> inhabited (U1 -> U2).
-Proof. intros [x2]; easy. Qed.
 
+Section Inhabited_Facts.
+
+Context {T1 T2 : Type}.
+Variable f g : T1 -> T2.
+
+Lemma fun_to_nonempty_compat : inhabited T2 -> inhabited (T1 -> T2).
+Proof. intros [x2]; apply (inhabits (fun=> x2)). Qed.
+
+(* TODO FC (09/02/2024): use unit_type. *)
 Lemma fun_to_singl_is_singl :
-  forall f g : U1 -> U2, inhabited U2 -> (forall x2 y2 : U2, x2 = y2) -> f = g.
+  inhabited T2 -> (forall x2 y2 : T2, x2 = y2) -> f = g.
 Proof. intros; apply fun_ext; intro; auto. Qed.
 
-Lemma fun_from_empty_is_nonempty : ~ inhabited U1 -> inhabited (U1 -> U2).
+Lemma fun_from_empty_is_nonempty : ~ inhabited T1 -> inhabited (T1 -> T2).
 Proof.
-intros HU1.
-destruct (choice (fun (_ : U1) (_ : U2) => True)); try easy.
-intros; contradict HU1; easy.
+intros HT1; destruct (choice (fun (_ : T1) (_ : T2) => True));
+    [intros; contradict HT1 |]; easy.
 Qed.
 
-Lemma fun_from_empty_is_singl :
-  forall (f g : U1 -> U2), ~ inhabited U1 -> f = g.
+(* TODO FC (09/02/2024): use unit_type. *)
+Lemma fun_from_empty_is_singl : ~ inhabited T1 -> f = g.
 Proof.
-intros f g; apply contra_not_l_equiv; intros H.
-apply (contra_not (fun_ext f g)), not_all_ex_not in H.
-destruct H as [x1 _]; apply (inhabits x1).
+apply contra_not_l_equiv;
+    move=> /fun_ext_contra_equiv [x1 _]; apply (inhabits x1).
 Qed.
 
-Definition fun_from_empty (HU1 : ~ inhabited U1) : U1 -> U2.
-Proof. intros; contradict HU1; easy. Qed.
+Definition fun_from_empty (HT1 : ~ inhabited T1) : T1 -> T2.
+Proof. intros; contradict HT1; easy. Qed.
 
 Lemma fun_to_empty_is_empty :
-  inhabited U1 -> ~ inhabited U2 -> ~ inhabited (U1 -> U2).
-Proof. intros [x1] HU2 [f]; contradict HU2; apply (inhabits (f x1)). Qed.
+  inhabited T1 -> ~ inhabited T2 -> ~ inhabited (T1 -> T2).
+Proof. intros [x1] HT2 [h]; contradict HT2; apply (inhabits (h x1)). Qed.
 
-Lemma fun_ext_rev : forall (f g : U1 -> U2), f = g -> forall x1, f x1 = g x1.
-Proof. intros; subst; easy. Qed.
+End Inhabited_Facts.
 
-Lemma fun_ext_equiv :
-  forall (f g : U1 -> U2), f = g <-> forall x1, f x1 = g x1.
-Proof. intros; split; [apply fun_ext_rev | apply fun_ext]. Qed.
 
-End Function_Facts1.
+Section Swap_Def.
 
+Context {T1 T2 T3 : Type}.
+Variable f : T1 -> T2 -> T3.
 
-Section Function_Facts2.
+Definition swap : T2 -> T1 -> T3 := fun x2 x1 => f x1 x2.
 
-Lemma comp_correct :
-  forall {U V W : Type} (f : U -> V) (g : V -> W) x, (g \o f) x = g (f x).
-Proof. easy. Qed.
+End Swap_Def.
 
-Lemma comp_assoc :
-  forall {U V W X : Type} {f : U -> V} {g : V -> W} {h : W -> X},
-    h \o (g \o f) = (h \o g) \o f.
-Proof. easy. Qed.
 
-Definition swap {U1 U2 V : Type} (f : U1 -> U2 -> V) : U2 -> U1 -> V :=
-  fun x2 x1 => f x1 x2.
+Section Swap_Facts.
 
-Lemma swap_invol :
-  forall {U1 U2 V : Type} (f : U1 -> U2 -> V), swap (swap f) = f.
+Context {T1 T2 T3 : Type}.
+Variable f : T1 -> T2 -> T3.
+
+Lemma swap_invol : swap (swap f) = f.
 Proof. easy. Qed.
 
-End Function_Facts2.
+End Swap_Facts.
+
 
+Section Image_preimage_Facts1.
 
-Section Function_Def.
+Context {T : Type}.
+Variable f : T -> T.
+Variable A : T -> Prop.
 
-Context {U1 U2 : Type}.
+Lemma image_id : f = id -> image f A = A.
+Proof.
+intros; subst; apply subset_ext_equiv; split;
+    intros x Hx; [destruct Hx | apply: Im]; easy.
+Qed.
 
-Variable f : U1 -> U2.
+Lemma preimage_id : f = id -> preimage f A = A.
+Proof. intros; subst; easy. Qed.
 
-Definition Rg : U2 -> Prop := image f fullset.
+End Image_preimage_Facts1.
 
-Definition surjective : Prop := forall x2, exists x1, f x1 = x2.
 
-End Function_Def.
+Section Image_preimage_Facts2.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
+Hypothesis H : cancel f g.
+
+Lemma image_cancel : cancel (image f) (image g).
+Proof. move=>>; rewrite -image_compose; apply image_id, fun_ext, H. Qed.
 
+Lemma image_inj : injective (image f).
+Proof.
+intros A1 B1 H1; rewrite -(image_cancel A1) -(image_cancel B1) H1; easy.
+Qed.
+
+Lemma preimage_cancel : cancel (preimage g) (preimage f).
+Proof. move=>>; rewrite -preimage_compose; apply preimage_id, fun_ext, H. Qed.
+
+Lemma preimage_inj : injective (preimage g).
+Proof.
+intros A2 B2 H1; rewrite -(preimage_cancel A2) -(preimage_cancel B2) H1; easy.
+Qed.
+
+End Image_preimage_Facts2.
+
+
+Section Image_preimage_Facts3.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
+Hypothesis H1 : cancel f g.
+Hypothesis H2 : cancel g f.
+
+Lemma preimage_eq : forall (A2 : T2 -> Prop), preimage f A2 = image g A2.
+Proof.
+move=>>; apply (preimage_inj H1); rewrite (preimage_cancel H2).
+apply eq_sym, preimage_of_image_equiv; eexists; apply (preimage_cancel H2).
+Qed.
+
+End Image_preimage_Facts3.
+
+
+Section Range_Def.
 
-Section Function_Facts3.
+Context {T1 T2 : Type}.
+Variable f : T1 -> T2.
 
-Context {U1 U2 : Type}.
+Definition Rg : T2 -> Prop := image f fullset.
 
-Context {f : U1 -> U2}.
+Definition surjective : Prop := forall x2, exists x1, f x1 = x2.
+
+End Range_Def.
+
+
+Section Range_Facts1.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
 
 Lemma Rg_correct : forall {x2} x1, x2 = f x1 -> Rg f x2.
 Proof. intros x2 x1; unfold Rg; rewrite image_eq; exists x1; easy. Qed.
@@ -147,15 +256,14 @@ Qed.
 Lemma surj_equiv_alt : surjective f <-> incl fullset (Rg f).
 Proof. rewrite surj_equiv; apply Rg_full_equiv. Qed.
 
-End Function_Facts3.
-
+End Range_Facts1.
 
-Section Function_Facts4a.
 
-Context {U1 U2 U3 : Type}.
+Section Range_Facts2.
 
-Context {f : U1 -> U2}.
-Context {g : U2 -> U3}.
+Context {T1 T2 T3 : Type}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma preimage_Rg : preimage f (Rg f) = fullset.
 Proof. apply preimage_of_image_full. Qed.
@@ -166,15 +274,30 @@ apply subset_ext_equiv; split; [intros _ [x2 _]; easy |].
 intros _ [_ [x1 _]]; apply: Im; easy.
 Qed.
 
-End Function_Facts4a.
+End Range_Facts2.
+
+
+Section Comp_Facts1.
 
+Context {T1 T2 T3 T4 : Type}.
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
+Variable h : T3 -> T4.
 
-Section Function_Facts4b.
+Lemma comp_correct : forall x, (g \o f) x = g (f x).
+Proof. easy. Qed.
+
+Lemma comp_assoc : h \o (g \o f) = (h \o g) \o f.
+Proof. easy. Qed.
+
+End Comp_Facts1.
 
-Context {U1 U2 : Type}.
 
-Context {f : U1 -> U2}.
-Context {g : U2 -> U1}.
+Section Comp_Facts2.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T1}.
 
 Lemma cancel_id : cancel f g <-> g \o f = id.
 Proof. apply iff_sym, fun_ext_equiv. Qed.
@@ -182,129 +305,135 @@ Proof. apply iff_sym, fun_ext_equiv. Qed.
 Lemma can_surj : cancel g f -> surjective f.
 Proof. intros H x1; exists (g x1); easy. Qed.
 
-End Function_Facts4b.
+End Comp_Facts2.
 
 
-Section Function_Facts4c.
+Section Comp_Facts3.
 
-Context {U1 U2 : Type}.
+Context {T1 T2 : Type}.
+Variable f : T1 -> T2.
 
-Context {f : U1 -> U2}.
-Hypothesis Hf : injective f.
+Lemma comp_id_l : id \o f = f.
+Proof. easy. Qed.
 
-Lemma inj_contra : forall x1 y1, x1 <> y1 -> f x1 <> f y1.
-Proof. move=>>; rewrite -contra_equiv; apply Hf. Qed.
+Lemma comp_id_r : f \o id = f.
+Proof. easy. Qed.
 
-Lemma inj_equiv : forall x1 y1, f x1 = f y1 <-> x1 = y1.
-Proof. intros; split; [apply Hf | apply f_equal]. Qed.
+End Comp_Facts3.
+
+
+Section Comp_Facts4.
+
+Context {T1 T2 T3 : Type}.
+Context {f : T2 -> T3}.
+Hypothesis Hf : injective f.
 
-End Function_Facts4c.
+Lemma comp_inj_r : forall {g h : T1 -> T2}, f \o g = f \o h -> g = h.
+Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
 
+End Comp_Facts4.
 
-Section Function_Facts4d.
 
-Context {U1 U2 U3 : Type}.
+Section Injective_Facts.
 
-Context {f : U2 -> U3}.
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
 Hypothesis Hf : injective f.
 
-Lemma inj_comp_l : forall (g h : U1 -> U2), f \o g = f \o h -> g = h.
-Proof. move=>> /fun_ext_rev H; apply fun_ext; intro; apply Hf, H. Qed.
+Lemma inj_contra : forall x1 y1, x1 <> y1 -> f x1 <> f y1.
+Proof. move=>>; rewrite -contra_equiv; apply Hf. Qed.
 
-End Function_Facts4d.
+Lemma inj_equiv : forall x1 y1, f x1 = f y1 <-> x1 = y1.
+Proof. intros; split; [apply Hf | apply f_equal]. Qed.
 
+End Injective_Facts.
 
-Section Function_Facts5.
 
-Context {U1 U2 : Type}.
+Section Inj_surj_bij_Facts1.
+
+Context {T1 T2 : Type}.
 
 Lemma fun_from_empty_is_inj :
-  forall (f : U1 -> U2), ~ inhabited U1 -> injective f.
-Proof. move=>> HU1 x1; contradict HU1; easy. Qed.
+  forall (f : T1 -> T2), ~ inhabited T1 -> injective f.
+Proof. move=>> HT1 x1; contradict HT1; easy. Qed.
 
 Lemma im_dec :
-  forall (f : U1 -> U2) x2, {x1 | x2 = f x1} + {forall x1, x2 <> f x1}.
+  forall (f : T1 -> T2) x2, { x1 | x2 = f x1 } + { forall x1, x2 <> f x1 }.
 Proof.
-intros f x2.
-destruct (excluded_middle_informative (exists x1, x2 = f x1))
-    as [H1 | H1]; [left | right].
-apply constructive_indefinite_description; easy.
-apply not_ex_all_not; easy.
+intros f x2; destruct (in_dec (fun x2 => exists x1, x2 = f x1) x2) as [H1 | H1];
+    [left; apply ex_EX | right; apply not_ex_all_not]; easy.
 Qed.
 
 Lemma inj_has_left_inv :
-  forall {f : U1 -> U2}, inhabited U1 -> injective f <-> exists g, cancel f g.
+  forall {f : T1 -> T2}, inhabited T1 -> injective f <-> exists g, cancel f g.
 Proof.
-intros f [a1]; split.
-(* *)
-intros Hf.
+intros f [a1]; split; [intros Hf | intros [g Hg]; apply: can_inj Hg].
 exists (fun x2 => match im_dec f x2 with
   | inleft H1 => proj1_sig H1
   | inright _ => a1
   end).
-intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1]; simpl.
-apply Hf; easy.
-contradict H1; apply nonempty_is_not_empty.
-exists x1; easy.
-(* *)
-intros [g Hg]; eapply can_inj, Hg.
+intros x1; destruct (im_dec f (f x1)) as [[y1 Hy1] | H1];
+    [apply Hf | contradict H1; rewrite not_all_not_ex_equiv; exists x1]; easy.
 Qed.
 
 Lemma surj_has_right_inv :
-  forall {f : U1 -> U2}, surjective f <-> exists g, cancel g f.
+  forall {f : T1 -> T2}, surjective f <-> exists g, cancel g f.
 Proof.
-intros; apply iff_sym; split. intros [g Hg]; eapply can_surj, Hg.
+intros; apply iff_sym; split; [intros [g Hg]; eapply can_surj, Hg |].
 intros Hf; destruct (choice _ Hf) as [g Hg]; exists g; easy.
 Qed.
 
-Lemma bij_surj : forall (f : U1 -> U2), bijective f -> surjective f.
-Proof.
-intros f [g _ H] x2; exists (g x2); apply H.
-Qed.
+Lemma bij_surj : forall (f : T1 -> T2), bijective f -> surjective f.
+Proof. intros f [g _ H] x2; exists (g x2); apply H. Qed.
 
 Lemma bij_equiv :
-  forall {f : U1 -> U2}, bijective f <-> injective f /\ surjective f.
+  forall {f : T1 -> T2}, bijective f <-> injective f /\ surjective f.
 Proof.
-intros f; split.
-intros Hf; split; [apply bij_inj | apply bij_surj]; easy.
-intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg].
-eapply Bijective; try easy; intros x1; auto.
+intros; split; [intros Hf; split; [apply bij_inj | apply bij_surj]; easy |].
+intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg];
+    apply: (Bijective _ Hg); intro; auto.
 Qed.
 
 Lemma bij_ex_uniq :
-  forall (f : U1 -> U2), bijective f <-> forall x2, exists! x1, f x1 = x2.
+  forall (f : T1 -> T2), bijective f <-> forall x2, exists! x1, f x1 = x2.
 Proof.
 intros f; rewrite bij_equiv; split.
 (* *)
-intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1]; exists x1; split; try easy.
+intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1]; exists x1; split; [easy |].
 intros y1 Hy1; apply Hf1; rewrite Hy1; easy.
 (* *)
-intros Hf; split.
-(* . *)
+intros Hf; split;
+    [| intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; exists x1; easy].
 intros x1 y1 H1; destruct (Hf (f x1)) as [x2 [Hx2a Hx2b]].
-rewrite -(Hx2b x1); try easy; apply Hx2b; symmetry; easy.
-(* . *)
-intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; exists x1; easy.
+rewrite -(Hx2b x1); [apply Hx2b, eq_sym |]; easy.
 Qed.
 
-End Function_Facts5.
+End Inj_surj_bij_Facts1.
+
 
+Section Inj_surj_bij_Facts2.
 
-Section Function_Facts6a.
+Context {T : Type}.
 
-Context {U1 U2 : Type}.
+Lemma surj_id : surjective (@id T).
+Proof. intros x; exists x; easy. Qed.
 
-Context {f : U1 -> U2}.
+Lemma bij_id : bijective (@id T).
+Proof. apply bij_equiv; split; [apply inj_id | apply surj_id]. Qed.
 
+End Inj_surj_bij_Facts2.
+
+
+Section Inverse_Def.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
 Hypothesis Hf : bijective f.
 
-Lemma f_inv_EX : { g : U2 -> U1 | cancel f g /\ cancel g f }.
-Proof.
-apply constructive_indefinite_description.
-induction Hf as [g Hg1 Hg2]; exists g; easy.
-Qed.
+Lemma f_inv_EX : { g : T2 -> T1 | cancel f g /\ cancel g f }.
+Proof. apply ex_EX; induction Hf as [g Hg1 Hg2]; exists g; easy. Qed.
 
-Definition f_inv : U2 -> U1 := proj1_sig f_inv_EX.
+Definition f_inv : T2 -> T1 := proj1_sig f_inv_EX.
 
 Lemma f_inv_correct_l : cancel f f_inv.
 Proof. apply (proj2_sig f_inv_EX). Qed.
@@ -312,45 +441,52 @@ Proof. apply (proj2_sig f_inv_EX). Qed.
 Lemma f_inv_correct_r : cancel f_inv f.
 Proof. apply (proj2_sig f_inv_EX). Qed.
 
-Lemma f_inv_uniq_l : forall (g : U2 -> U1), cancel f g -> g = f_inv.
+End Inverse_Def.
+
+
+Section Inverse_Facts1.
+
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
+Hypothesis Hf : bijective f.
+
+Lemma f_inv_uniq_l : forall (g : T2 -> T1), cancel f g -> g = f_inv Hf.
 Proof.
 intros; apply fun_ext, (bij_can_eq Hf); [easy | apply f_inv_correct_l].
 Qed.
 
-Lemma f_inv_uniq_r : forall (g : U2 -> U1), cancel g f -> g = f_inv.
+Lemma f_inv_uniq_r : forall (g : T2 -> T1), cancel g f -> g = f_inv Hf.
 Proof.
 move=>> Hg; apply fun_ext, (inj_can_eq Hg);
     [apply bij_inj; easy | apply f_inv_correct_r].
 Qed.
 
-Lemma f_inv_bij : bijective f_inv.
+Lemma f_inv_bij : bijective (f_inv Hf).
 Proof. apply (bij_can_bij Hf), f_inv_correct_l. Qed.
 
-Lemma f_inv_inj : injective f_inv.
+Lemma f_inv_inj : injective (f_inv Hf).
 Proof. apply bij_inj, f_inv_bij. Qed.
 
-Lemma f_inv_surj : surjective f_inv.
+Lemma f_inv_surj : surjective (f_inv Hf).
 Proof. apply bij_surj, f_inv_bij. Qed.
 
-Lemma f_inv_eq_equiv : forall x1 x2, f_inv x2 = x1 <-> x2 = f x1.
+Lemma f_inv_eq_equiv : forall x1 x2, f_inv Hf x2 = x1 <-> x2 = f x1.
 Proof.
 intros x1 x2; split.
-rewrite -{2}(f_inv_correct_r x2); apply f_equal.
-rewrite -{2}(f_inv_correct_l x1); apply f_equal.
+rewrite -{2}(f_inv_correct_r Hf x2); apply f_equal.
+rewrite -{2}(f_inv_correct_l Hf x1); apply f_equal.
 Qed.
 
-Lemma f_inv_neq_equiv : forall x1 x2, f_inv x2 <> x1 <-> x2 <> f x1.
+Lemma f_inv_neq_equiv : forall x1 x2, f_inv Hf x2 <> x1 <-> x2 <> f x1.
 Proof. intros; rewrite -iff_not_equiv; apply f_inv_eq_equiv. Qed.
 
-End Function_Facts6a.
-
-
-Section Function_Facts6b.
+End Inverse_Facts1.
 
-Context {U1 U2 : Type}.
 
-Context {f : U1 -> U2}.
+Section Inverse_Facts2.
 
+Context {T1 T2 : Type}.
+Context {f : T1 -> T2}.
 Hypothesis Hf : bijective f.
 
 Lemma f_inv_invol : forall (Hf1 : bijective (f_inv Hf)), f_inv Hf1 = f.
@@ -359,91 +495,31 @@ Proof. intros; apply sym_eq, f_inv_uniq_l, f_inv_correct_r. Qed.
 Lemma f_inv_invol_alt : f_inv (f_inv_bij Hf) = f.
 Proof. apply f_inv_invol. Qed.
 
-Context {g : U1 -> U2}.
-
+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.
 
-End Function_Facts6b.
-
+End Inverse_Facts2.
 
-Section Function_Facts6c.
 
-Context {U : Type}.
-
-Context {f : U -> U}.
+Section Inverse_Facts3.
 
+Context {T : Type}.
+Context {f : T -> T}.
 Hypothesis Hf : bijective f.
 
 Lemma f_inv_id : involutive f -> f_inv Hf = f.
 Proof.
-intros; apply (inj_comp_l (bij_inj Hf)).
-apply fun_ext; intro; unfold comp; rewrite H f_inv_correct_r; easy.
-Qed.
-
-End Function_Facts6c.
-
-
-Section Function_Facts7.
-
-Lemma bij_id : forall {T : Type}, bijective (@id T).
-Proof.
-intros; apply bij_equiv; split. apply inj_id. intros x; exists x; easy.
+intros; apply (comp_inj_r (bij_inj Hf)).
+apply fun_ext; intro; rewrite !comp_correct H f_inv_correct_r; easy.
 Qed.
 
-Lemma comp_id_l : forall {U V : Type} (f : U -> V), id \o f = f.
-Proof. easy. Qed.
-
-Lemma comp_id_r : forall {U V : Type} (f : U -> V), f \o id = f.
-Proof. easy. Qed.
-
-Lemma preimage_id :
-  forall {U : Type} (f : U -> U) (A : U -> Prop), f = id -> preimage f A = A.
-Proof. intros; subst; easy. Qed.
+Lemma f_inv_id_rev : f_inv Hf = f -> involutive f.
+Proof. intros H x; rewrite -{1}H; apply f_inv_correct_l. Qed.
 
-Lemma preimage_cancel :
-  forall {U1 U2 : Type} {f : U1 -> U2} {g : U2 -> U1},
-    cancel f g -> cancel (preimage g) (preimage f).
-Proof.
-move=>> H A1; rewrite -preimage_compose; apply preimage_id, fun_ext, H.
-Qed.
-
-Lemma preimage_inj :
-  forall {U1 U2 : Type} {f : U1 -> U2} {g : U2 -> U1},
-    cancel g f -> injective (preimage f).
-Proof.
-move=>> H A2 B2 H2;
-    rewrite -(preimage_cancel H A2) -(preimage_cancel H B2) H2; easy.
-Qed.
-
-Lemma preimage_eq :
-  forall {U1 U2 : Type} {f : U1 -> U2} {g : U2 -> U1} (A2 : U2 -> Prop),
-    cancel f g -> cancel g f -> preimage f A2 = image g A2.
-Proof.
-move=>> H1 H2; apply (preimage_inj H1); rewrite preimage_cancel//.
-apply sym_eq, preimage_of_image_equiv; eexists; apply (preimage_cancel H2).
-Qed.
-
-Lemma image_id :
-  forall {U : Type} (f : U -> U) (A : U -> Prop), f = id -> image f A = A.
-Proof.
-intros; subst; apply subset_ext_equiv; split;
-    intros x Hx; [destruct Hx | apply: Im]; easy.
-Qed.
-
-Lemma image_cancel :
-  forall {U1 U2 : Type} {f : U1 -> U2} {g : U2 -> U1},
-    cancel f g -> cancel (image f) (image g).
-Proof. move=>> H A1; rewrite -image_compose; apply image_id, fun_ext, H. Qed.
-
-Lemma image_inj :
-  forall {U1 U2 : Type} {f : U1 -> U2} {g : U2 -> U1},
-    cancel f g -> injective (image f).
-Proof.
-move=>> H A1 B1 H1;
-    rewrite -(image_cancel H A1) -(image_cancel H B1) H1; easy.
-Qed.
+Lemma f_inv_id_equiv : f_inv Hf = f <-> involutive f.
+Proof. split; [apply f_inv_id_rev | apply f_inv_id]. Qed.
 
-End Function_Facts7.
+End Inverse_Facts3.
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index 007615ed8360c29307cc11900263b2de1e51fa34..f4b7dc339154fd8a09f497694ff16ec458bcc824 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -14,109 +14,113 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import ClassicalEpsilon Morphisms.
-From Coq Require Import ssreflect ssrfun ssrbool.
+(* We need unique choice. *)
+From Coq Require Import (*ClassicalUniqueChoice*) ClassicalChoice.
+From Coq Require Import ssreflect ssrfun.
 
 From Lebesgue Require Import Subset Subset_dec Function.
 
-From FEM Require Import Function_compl.
+From FEM Require Import logic_compl Function_compl.
+
+
+(** Support for restrictions of functions to subsets. *)
 
 
 Section Function_sub_Def0.
 
-Context {E F : Type}.
+Context {T1 T2 : Type}.
 
-Variable PE : E -> Prop.
-Variable PF : F -> Prop.
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
 
-Variable f : E -> F.
+Variable f : T1 -> T2.
 
-Definition RgS := image f PE.
-Definition RgS_gen := inter PF RgS.
+Definition RgS := image f P1.
+Definition RgS_gen := inter P2 RgS.
 
-(* The range of function f on subset PE is in subset PF.
- This property makes the restriction of f from subset PE to subset PF
+(* 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 PF.
+Definition funS : Prop := incl RgS P2.
 
-(* The function f is injective on subset PE. *)
+(* The function f is injective on subset P1. *)
 Definition injS : Prop :=
-  forall x1 x2, PE x1 -> PE x2 -> f x1 = f x2 -> x1 = x2.
+  forall x1 x2, P1 x1 -> P1 x2 -> f x1 = f x2 -> x1 = x2.
 
-(* The function f is surjective from subset PE onto subset PF. *)
-Definition surjS : Prop := forall y, PF y -> exists x, PE x /\ f x = y.
+(* The function f is surjective from subset P1 onto subset P2. *)
+Definition surjS : Prop := forall y, P2 y -> exists x, P1 x /\ f x = y.
 
-(* The function f is bijjective from subset PE onto subset PF. *)
+(* The function f is bijjective from subset P1 onto subset P2. *)
 Definition bijS : Prop :=
-  funS /\ (forall y, PF y -> exists! x, PE x /\ f x = y).
+  funS /\ (forall y, P2 y -> exists! x, P1 x /\ f x = y).
 
-Variable f1 : F -> E.
+Variable f1 : T2 -> T1.
 
-(* The function f1 cancels the function f on subset PE,
- ie it is the left inverse of function f on subset PE. *)
-Definition canS : Prop := forall x, PE x -> f1 (f x) = x.
+(* The function f1 cancels the function f on subset P1,
+ ie it is the left inverse of function f on subset P1. *)
+Definition canS : Prop := forall x, P1 x -> f1 (f x) = x.
 
 End Function_sub_Def0.
 
 
 Section Function_sub_Def1.
 
-Context {E F : Type}.
+Context {T1 T2 : Type}.
 
-Variable PE : E -> Prop.
-Variable PF : F -> Prop.
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
 
-Variable f : E -> F.
-Variable f1 : F -> E.
+Variable f : T1 -> T2.
+Variable f1 : T2 -> T1.
 
 Definition bijS_alt : Prop :=
-  funS PE PF f /\ funS PF PE f1 /\ canS PE f f1 /\ canS PF f1 f.
+  funS P1 P2 f /\ funS P2 P1 f1 /\ canS P1 f f1 /\ canS P2 f1 f.
 
 End Function_sub_Def1.
 
 
 Section Function_sub_Facts0a.
 
-Context {E F : Type}.
+Context {T1 T2 : Type}.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma RgS_eq : RgS PE f = RgS_gen PE (RgS PE f) f.
+Lemma RgS_eq : RgS P1 f = RgS_gen P1 (RgS P1 f) f.
 Proof. apply sym_eq, inter_idem. Qed.
 
-Lemma RgS_correct : forall {v} u, PE u -> v = f u -> RgS PE f v.
+Lemma RgS_correct : forall {v} u, P1 u -> v = f u -> RgS P1 f v.
 Proof. intros; subst; easy. Qed.
 
-Lemma RgS_ex : forall {v}, RgS PE f v <-> exists u, PE u /\ v = f u.
+Lemma RgS_ex : forall {v}, RgS P1 f v <-> exists u, P1 u /\ v = f u.
 Proof. intros; unfold RgS; rewrite image_eq; easy. Qed.
 
-Lemma RgS_gen_eq : funS PE PF f -> RgS_gen PE PF f = RgS PE f.
+Lemma RgS_gen_eq : funS P1 P2 f -> RgS_gen P1 P2 f = RgS P1 f.
 Proof. rewrite -inter_right; easy. Qed.
 
 Lemma RgS_gen_correct :
-  forall {v} u, PF v -> PE u -> v = f u -> RgS_gen PE PF f v.
+  forall {v} u, P2 v -> P1 u -> v = f u -> RgS_gen P1 P2 f v.
 Proof. intros; subst; easy. Qed.
 
 Lemma RgS_gen_ex :
-  forall {PF} {v}, RgS_gen PE PF f v <-> PF v /\ (exists u, PE u /\ v = f u).
+  forall {P2} {v}, RgS_gen P1 P2 f v <-> P2 v /\ (exists u, P1 u /\ v = f u).
 Proof. intros; rewrite -RgS_ex; easy. Qed.
 
-Lemma funS_correct : (forall x, PE x -> PF (f x)) -> funS PE PF f.
+Lemma funS_correct : (forall x, P1 x -> P2 (f x)) -> funS P1 P2 f.
 Proof. intros Hf _ [x Hx]; auto. Qed.
 
-Lemma funS_rev : funS PE PF f -> forall x, PE x -> PF (f x).
+Lemma funS_rev : funS P1 P2 f -> forall x, P1 x -> P2 (f x).
 Proof. intros Hf x Hx; apply Hf; easy. Qed.
 
-Lemma funS_equiv : funS PE PF f <-> forall x, PE x -> PF (f x).
+Lemma funS_equiv : funS P1 P2 f <-> forall x, P1 x -> P2 (f x).
 Proof. split; [apply funS_rev | apply funS_correct]. Qed.
 
-Lemma surjS_correct : incl PF (RgS PE f) -> surjS PE PF f.
+Lemma surjS_correct : incl P2 (RgS P1 f) -> surjS P1 P2 f.
 Proof. intros Hf y Hy; destruct (Hf y Hy) as [x Hx]; exists x; easy. Qed.
 
-Lemma surjS_rev : surjS PE PF f -> RgS_gen PE PF f = PF.
+Lemma surjS_rev : surjS P1 P2 f -> RgS_gen P1 P2 f = P2.
 Proof.
 intros Hf; apply incl_antisym; intros v Hv; [apply Hv |].
 destruct (Hf _ Hv) as [u Hu]; apply (RgS_gen_correct u); easy.
@@ -127,17 +131,17 @@ End Function_sub_Facts0a.
 
 Section Function_sub_Facts0b.
 
-Context {E F : Type}.
+Context {T1 T2 : Type}.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma funS_id : funS PE PE id.
+Lemma funS_id : funS P1 P1 id.
 Proof. apply funS_equiv; easy. Qed.
 
-Lemma surjS_equiv : surjS PE PF f <-> RgS_gen PE PF f = PF.
+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.
@@ -148,27 +152,33 @@ End Function_sub_Facts0b.
 
 Section Function_sub_Facts0c.
 
-Context {E F : Type}.
-Hypothesis HE : inhabited E.
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma bijS_ex : bijS PE PF f <-> (exists f1, bijS_alt PE PF f f1).
+Lemma bijS_ex : bijS P1 P2 f <-> (exists f1, bijS_alt P1 P2 f f1).
 Proof.
 split.
 (* *)
 intros [Hfa Hfb].
-destruct (choice (fun y x => PF y -> PE x /\ f x = y)) as [f1 Hf1].
-  intros y; destruct (in_dec PF y) as [Hy | Hy].
+(* WIP.
+destruct (unique_choice (fun y x => P2 y -> P1 x /\ f x = y)) as [f1 Hf1].
+  intros y; destruct (in_dec P2 y) as [Hy | Hy].
+  destruct (Hfb y Hy) as [x [Hx1 Hx2]]; exists x; split; [easy |].
+  intros x'.
+*)
+destruct (choice (fun y x => P2 y -> P1 x /\ f x = y)) as [f1 Hf1].
+  intros y; destruct (in_dec P2 y) as [Hy | Hy].
   destruct (Hfb y Hy) as [x [Hx1 Hx2]]; exists x; easy.
-  destruct HE as [x]; exists x; easy.
+  destruct HT1 as [x]; exists x; easy.
 exists f1; repeat split; try easy.
 intros _ [x Hx]; apply Hf1; easy.
 2: intros y Hy; apply Hf1; easy.
-assert (Hf3 : injS PE f).
+assert (Hf3 : injS P1 f).
   intros x1 x2 Hx1 Hx2 Hx.
   destruct (Hfb (f x1)) as [x [Hxa Hxb]]; try now apply Hfa.
   rewrite -(Hxb x1); try apply Hxb; easy.
@@ -185,55 +195,55 @@ End Function_sub_Facts0c.
 
 Section Function_sub_Facts1.
 
-Context {E F G : Type}.
+Context {T1 T2 T3 : Type}.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
-Context {PG : G -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
+Context {P3 : T3 -> Prop}.
 
-Context {f : E -> F}.
-Context {g : F -> G}.
+Context {f : T1 -> T2}.
+Context {g : T2 -> T3}.
 
 Lemma RgS_full : RgS fullset f = Rg f.
 Proof. easy. Qed.
 
-Lemma RgS_gen_full_l : RgS_gen fullset PF f = inter PF (Rg f).
+Lemma RgS_gen_full_l : RgS_gen fullset P2 f = inter P2 (Rg f).
 Proof. easy. Qed.
 
-Lemma RgS_gen_full_r : forall {PE}, RgS_gen PE fullset f = RgS PE f.
+Lemma RgS_gen_full_r : forall {P1}, RgS_gen P1 fullset f = RgS P1 f.
 Proof. intros; unfold RgS_gen; rewrite inter_full_l; easy. Qed.
 
 Lemma RgS_gen_full : RgS_gen fullset fullset f = Rg f.
 Proof. rewrite RgS_gen_full_r RgS_full; easy. Qed.
 
-Lemma RgS_gen_full_equiv : RgS_gen PE PF f = PF <-> incl PF (RgS PE f).
+Lemma RgS_gen_full_equiv : RgS_gen P1 P2 f = P2 <-> incl P2 (RgS P1 f).
 Proof. symmetry; apply inter_left. Qed.
 
 Lemma RgS_gen_full_equiv_alt :
-  funS PE PF f -> RgS_gen PE PF f = PF <-> RgS PE f = PF.
+  funS P1 P2 f -> RgS_gen P1 P2 f = P2 <-> RgS P1 f = P2.
 Proof. rewrite RgS_gen_full_equiv subset_ext_equiv; easy. Qed.
 
-Lemma RgS_preimage : RgS (preimage f PF) f = inter PF (Rg f).
+Lemma RgS_preimage : RgS (preimage f P2) f = inter P2 (Rg f).
 Proof. apply image_of_preimage. Qed.
 
-Lemma RgS_preimage_equiv : RgS (preimage f PF) f = PF <-> incl PF (Rg f).
+Lemma RgS_preimage_equiv : RgS (preimage f P2) f = P2 <-> incl P2 (Rg f).
 Proof. rewrite RgS_preimage -inter_left; easy. Qed.
 
-Lemma RgS_preimage_RgS : RgS (preimage f (RgS PE f)) f = RgS PE f.
+Lemma RgS_preimage_RgS : RgS (preimage f (RgS P1 f)) f = RgS P1 f.
 Proof. apply image_of_preimage_of_image. Qed.
 
-Lemma preimage_RgS : incl PE (preimage f (RgS PE f)).
+Lemma preimage_RgS : incl P1 (preimage f (RgS P1 f)).
 Proof. apply preimage_of_image. Qed.
 
 Lemma preimage_RgS_equiv :
-  preimage f (RgS PE f) = PE <-> exists PF, preimage f PF = PE.
+  preimage f (RgS P1 f) = P1 <-> exists P2, preimage f P2 = P1.
 Proof. apply preimage_of_image_equiv. Qed.
 
 Lemma preimage_RgS_preimage :
-  preimage f (RgS (preimage f PF) f) = preimage f PF.
+  preimage f (RgS (preimage f P2) f) = preimage f P2.
 Proof. apply preimage_of_image_of_preimage. Qed.
 
-Lemma RgS_comp : RgS PE (g \o f) = RgS (RgS PE f) g.
+Lemma RgS_comp : RgS P1 (g \o f) = RgS (RgS P1 f) g.
 Proof.
 apply subset_ext_equiv; split; intros z;
     [intros [x Hx] | intros [y [x Hx]]; fold ((g \o f) x)]; easy.
@@ -243,24 +253,24 @@ Lemma Rg_comp_alt : Rg (g \o f) = RgS (Rg f) g.
 Proof. apply Rg_comp. Qed.
 
 Lemma funS_full_l :
-  forall PF (f : E -> F), incl (Rg f) PF -> funS fullset PF f.
+  forall P2 (f : T1 -> T2), incl (Rg f) P2 -> funS fullset P2 f.
 Proof. easy. Qed.
 
-Lemma funS_full_r : forall PE (f : E -> F), funS PE fullset f.
+Lemma funS_full_r : forall P1 (f : T1 -> T2), funS P1 fullset f.
 Proof. easy. Qed.
 
-Lemma funS_full : forall (f : E -> F), funS fullset fullset f.
+Lemma funS_full : forall (f : T1 -> T2), funS fullset fullset f.
 Proof. easy. Qed.
 
 Lemma funS_comp :
-  forall PF PG (f : E -> F) (g : F -> G),
-    funS PE PF f -> funS PF PG g -> funS PE PG (g \o f).
+  forall P2 P3 (f : T1 -> T2) (g : T2 -> T3),
+    funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
 Proof.
-intros PF1 PG1 f1 g1 Hf1 Hg1 z [x Hx]; rewrite comp_correct;
+intros P21 P31 f1 g1 Hf1 Hg1 z [x Hx]; rewrite comp_correct;
     apply Hg1, (RgS_correct (f1 x)); [apply Hf1; apply (RgS_correct x) |]; easy.
 Qed.
 
-Lemma surjS_equiv_alt : surjS PE PF f <-> incl PF (RgS PE f).
+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.
@@ -268,31 +278,31 @@ End Function_sub_Facts1.
 
 Section Function_sub_Facts2a.
 
-Context {E F : Type}.
-Hypothesis HE : inhabited E.
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma bijS_funS : bijS PE PF f -> funS PE PF f.
+Lemma bijS_funS : bijS P1 P2 f -> funS P1 P2 f.
 Proof. unfold bijS; easy. Qed.
 
-Lemma bijS_injS : forall PF {f : E -> F}, bijS PE PF f -> injS PE f.
+Lemma bijS_injS : forall P2 {f : T1 -> T2}, bijS P1 P2 f -> injS P1 f.
 Proof.
-move=>> /(bijS_ex HE) [f1 [Hf [_ [Hfl _]]]] x y Hx Hy H;
+move=>> /(bijS_ex HT1) [f1 [Hf [_ [Hfl _]]]] x y Hx Hy H;
     rewrite -(Hfl x)// -(Hfl y)// H; easy.
 Qed.
 
-Lemma bijS_surjS : bijS PE PF f -> surjS PE PF f.
+Lemma bijS_surjS : bijS P1 P2 f -> surjS P1 P2 f.
 Proof.
-move=> /(bijS_ex HE) [f1 [_ [/funS_equiv Hf1 [_ Hfr]]]] y Hy;
+move=> /(bijS_ex HT1) [f1 [_ [/funS_equiv Hf1 [_ Hfr]]]] y Hy;
     exists (f1 y); auto.
 Qed.
 
 Lemma injS_surjS_bijS :
-  funS PE PF f -> injS PE f -> surjS PE PF f -> bijS PE PF f.
+  funS P1 P2 f -> injS P1 f -> surjS P1 P2 f -> bijS P1 P2 f.
 Proof.
 intros Hf1a Hf1b Hf2; split; try easy.
 intros y Hy; destruct (Hf2 _ Hy) as [x1 Hx1]; exists x1; split; try easy.
@@ -300,10 +310,10 @@ intros x2 Hx2; apply Hf1b; try easy.
 apply trans_eq with y; easy.
 Qed.
 
-Lemma bijS_equiv : bijS PE PF f <-> funS PE PF f /\ injS PE f /\ surjS PE PF f.
+Lemma bijS_equiv : bijS P1 P2 f <-> funS P1 P2 f /\ injS P1 f /\ surjS P1 P2 f.
 Proof.
 split; intros Hf; [split; [apply bijS_funS; easy |] |].
-split; [apply (bijS_injS PF) | apply bijS_surjS]; easy.
+split; [apply (bijS_injS P2) | apply bijS_surjS]; easy.
 apply injS_surjS_bijS; easy.
 Qed.
 
@@ -312,18 +322,18 @@ End Function_sub_Facts2a.
 
 Section Function_sub_Facts2b.
 
-Context {E F : Type}.
-Hypothesis HE : inhabited E.
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma surjS_RgS : forall PE (f : E -> F), surjS PE (RgS PE f) f.
+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 PE (RgS PE f) f <-> injS PE f.
+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.
@@ -334,13 +344,13 @@ End Function_sub_Facts2b.
 
 Section Function_sub_Facts3.
 
-Context {E F : Type}.
-Hypothesis HE : inhabited E.
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
 
-Variable PE : E -> Prop.
-Variable PF : F -> Prop.
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
 
-Variable f : E -> F.
+Variable f : T1 -> T2.
 
 Lemma inj_S_equiv : injective f <-> injS fullset f.
 Proof. split; intros Hf; move=>>; [auto | apply Hf; easy]. Qed.
@@ -360,35 +370,32 @@ End Function_sub_Facts3.
 
 Section Function_sub_Facts4.
 
-Context {E F : Type}.
-Hypothesis HE : inhabited E.
-Hypothesis HF : inhabited F.
+Context {T1 T2 : Type}.
+Hypothesis HT1 : inhabited T1.
+Hypothesis HT2 : inhabited T2.
 
-Context {PE : E -> Prop}.
-Context {PF : F -> Prop}.
+Context {P1 : T1 -> Prop}.
+Context {P2 : T2 -> Prop}.
 
-Context {f : E -> F}.
+Context {f : T1 -> T2}.
 
-Lemma f_invS_EX : bijS PE PF f -> { f1 : F -> E | bijS_alt PE PF f f1 }.
-Proof.
-intros Hf; apply constructive_indefinite_description.
-apply bijS_ex; easy.
-Qed.
+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.
 
-Definition f_invS (Hf : bijS PE PF f) := proj1_sig (f_invS_EX Hf).
+Definition f_invS (Hf : bijS P1 P2 f) := proj1_sig (f_invS_EX Hf).
 
-Hypothesis Hf : bijS PE PF f.
+Hypothesis Hf : bijS P1 P2 f.
 
-Lemma f_invS_funS_l : funS PE PF f.
+Lemma f_invS_funS_l : funS P1 P2 f.
 Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
 
-Lemma f_invS_funS_r : funS PF PE (f_invS Hf).
+Lemma f_invS_funS_r : funS P2 P1 (f_invS Hf).
 Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
 
-Lemma f_invS_canS_l : canS PF (f_invS Hf) f.
+Lemma f_invS_canS_l : canS P2 (f_invS Hf) f.
 Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
 
-Lemma f_invS_canS_r : canS PE f (f_invS Hf).
+Lemma f_invS_canS_r : canS P1 f (f_invS Hf).
 Proof. apply (proj2_sig (f_invS_EX Hf)). Qed.
 
 End Function_sub_Facts4.
@@ -396,38 +403,38 @@ End Function_sub_Facts4.
 
 Section Function_sub_Facts5a.
 
-Context {E F G : Type}.
+Context {T1 T2 T3 : Type}.
 
-Variable PE : E -> Prop.
-Variable PF : F -> Prop.
-Variable PG : G -> Prop.
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
 
-Variable f : E -> F.
-Variable g : F -> G.
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
 
-Lemma funS_comp_compat : funS PE PF f -> funS PF PG g -> funS PE PG (g \o f).
+Lemma funS_comp_compat : funS P1 P2 f -> funS P2 P3 g -> funS P1 P3 (g \o f).
 Proof. move=> /funS_equiv Hf /funS_equiv Hg _ [x Hx]; apply Hg, Hf; easy. Qed.
 
 Lemma injS_comp_compat :
-  funS PE PF f -> injS PE f -> injS PF g -> injS PE (g \o f).
+  funS P1 P2 f -> injS P1 f -> injS P2 g -> injS P1 (g \o f).
 Proof.
 intros Hf0 Hf Hg x1 x2 Hx1 Hx2 Hx; apply Hf, Hg; try apply Hf0; easy.
 Qed.
 
-Lemma injS_comp_reg : injS PE (g \o f) -> injS PE f.
+Lemma injS_comp_reg : injS P1 (g \o f) -> injS P1 f.
 Proof.
 intros H x1 x2 Hx1 Hx2 Hx; apply H; try rewrite comp_correct Hx; easy.
 Qed.
 
 Lemma surjS_comp_compat :
-  surjS PE PF f -> surjS PF PG g -> surjS PE PG (g \o f).
+  surjS P1 P2 f -> surjS P2 P3 g -> surjS P1 P3 (g \o f).
 Proof.
 intros Hf Hg z Hz.
 destruct (Hg z Hz) as [y [Hy1 Hy2]], (Hf y Hy1) as [x [Hx1 Hx2]].
 exists x; split; [| rewrite comp_correct Hx2]; easy.
 Qed.
 
-Lemma surjS_comp_reg : funS PE PF f -> surjS PE PG (g \o f) -> surjS PF PG g.
+Lemma surjS_comp_reg : funS P1 P2 f -> surjS P1 P3 (g \o f) -> surjS P2 P3 g.
 Proof.
 intros Hf H z Hz; destruct (H z Hz) as [x [Hx1 Hx2]].
 exists (f x); split; try apply Hf; easy.
@@ -435,8 +442,8 @@ Qed.
 
 Lemma canS_comp_compat :
   forall {f1 g1},
-    funS PE PF f -> canS PE f f1 -> canS PF g g1 ->
-    canS PE (g \o f) (f1 \o 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 Hf1 Hg1 x Hx.
 rewrite -> !comp_correct, Hg1, Hf1; auto.
@@ -447,39 +454,39 @@ End Function_sub_Facts5a.
 
 Section Function_sub_Facts5b.
 
-Context {E F G : Type}.
-Hypothesis HE : inhabited E.
-Hypothesis HF : inhabited F.
+Context {T1 T2 T3 : Type}.
+Hypothesis HT1 : inhabited T1.
+Hypothesis HT2 : inhabited T2.
 
-Variable PE : E -> Prop.
-Variable PF : F -> Prop.
-Variable PG : G -> Prop.
+Variable P1 : T1 -> Prop.
+Variable P2 : T2 -> Prop.
+Variable P3 : T3 -> Prop.
 
-Variable f : E -> F.
-Variable g : F -> G.
+Variable f : T1 -> T2.
+Variable g : T2 -> T3.
 
 Lemma bijS_alt_comp_compat :
   forall f1 g1,
-    bijS_alt PE PF f f1 -> bijS_alt PF PG g g1 ->
-    bijS_alt PE PG (g \o f) (f1 \o g1).
+    bijS_alt P1 P2 f f1 -> bijS_alt P2 P3 g g1 ->
+    bijS_alt P1 P3 (g \o f) (f1 \o g1).
 Proof.
 intros f1 g1 [Hf1 [Hf2 [Hf3 Hf4]]] [Hg1 [Hg2 [Hg3 Hg4]]]; repeat split.
-1,2: apply funS_comp_compat with PF; easy.
-1,2: apply canS_comp_compat with PF; easy.
+1,2: apply funS_comp_compat with P2; easy.
+1,2: apply canS_comp_compat with P2; easy.
 Qed.
 
-Lemma bijS_comp_compat : bijS PE PF f -> bijS PF PG g -> bijS PE PG (g \o f).
+Lemma bijS_comp_compat : bijS P1 P2 f -> bijS P2 P3 g -> bijS P1 P3 (g \o f).
 Proof.
-move=> /(bijS_ex HE) [f1 Hf1] /(bijS_ex HF) [g1 Hg1].
-apply (bijS_ex HE); exists (f1 \o g1).
+move=> /(bijS_ex HT1) [f1 Hf1] /(bijS_ex HT2) [g1 Hg1].
+apply (bijS_ex HT1); exists (f1 \o g1).
 apply bijS_alt_comp_compat; easy.
 Qed.
 
 Lemma bijS_comp_reg :
-  funS PE PF f -> bijS PE PG (g \o f) -> injS PE f /\ surjS PF PG g.
+  funS P1 P2 f -> bijS P1 P3 (g \o f) -> injS P1 f /\ surjS P2 P3 g.
 Proof.
-intros H0 H1; move: (proj1 (bijS_equiv HE) H1) => [H2 H3]; split;
-    [apply injS_comp_reg with g | apply surjS_comp_reg with PE f]; easy.
+intros H0 H1; move: (proj1 (bijS_equiv HT1) H1) => [H2 H3]; split;
+    [apply injS_comp_reg with g | apply surjS_comp_reg with P1 f]; easy.
 Qed.
 
 End Function_sub_Facts5b.
diff --git a/FEM/Compl/Subset_compl.v b/FEM/Compl/Subset_compl.v
index 3cd208ed4904ef66179013bb4ff766f0cca021f3..85f38a50e2c730659db5281c346200ae68a7a36b 100644
--- a/FEM/Compl/Subset_compl.v
+++ b/FEM/Compl/Subset_compl.v
@@ -14,124 +14,151 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import ClassicalEpsilon Reals.
-From Coq Require Import ssreflect ssrfun ssrbool.
+From Coq Require Import ssreflect ssrfun.
 
-From Lebesgue Require Import Subset Subset_charac.
+(* We need decidability of the emptiness of subsets. *)
+From Lebesgue Require Import Subset Subset_dec Subset_charac.
 
+(* We need a constructive form of indefinite description. *)
+From FEM Require Import logic_compl.
+
+
+(** Additional definitions and results about subsets.
+  This complements the file Lebesgue.Subset.
+
+  Support for inhabitated types.
+  'elem_of' provides an element of any inhabitated type.
+  'elem_of_subset' provides an element of any nonempty subset of any type.
+
+  Support for unit types.
+  'unit_type x' states that all elements of the type are equal to x.
+  'is_unit_type' is the predicate stating that a type has only one element.
+  'unit_subset_dec' is a decidability result stating that subsets of unit types
+    are either empty or singletons.
+  'unit_subset_is_singleton' states the condition for subsets of unit types
+    to be singletons.
+
+  Some additional properties of union and inter.
+  '{union,inter}_inj_{l,r}' state the condition for the corresponding operator
+    to be injective wrt its first (left) or second (right) argument.
+*)
 
-Section Subset_Facts.
 
-Definition elem_of {U : Type} (HU : inhabited U) : U.
+Section Subset_Def1.
+
+Context {T : Type}.
+
+Definition elem_of (HT : inhabited T) : T.
 Proof.
-assert (H : { x : U | True}).
-  apply constructive_indefinite_description; destruct HU; easy.
+assert (H : { x : T | True}) by now apply ex_EX; destruct HT.
 destruct H; easy.
 Qed.
 
-Definition elem_of_subset
-    {U : Type} {PU : U -> Prop} (HPU : nonempty PU) : U :=
-  proj1_sig (constructive_indefinite_description PU HPU).
+Definition elem_of_subset {A : T -> Prop} (HA : nonempty A) : T :=
+  proj1_sig (ex_EX A HA).
 
 Lemma elem_of_subset_correct :
-  forall {U : Type} {PU : U -> Prop} (HPU : nonempty PU),
-    PU (elem_of_subset HPU).
-Proof.
-intros; apply (proj2_sig (constructive_indefinite_description _ _)).
-Qed.
+  forall {A : T -> Prop} (HA : nonempty A), A (elem_of_subset HA).
+Proof. intros; apply (proj2_sig (ex_EX _ _)). Qed.
+
+End Subset_Def1.
+
 
-Definition unit_type {U : Type} (x : U) : Prop := forall y : U, y = x.
-Definition is_unit_type (U : Type) : Prop := exists x : U, unit_type x.
+Section Subset_Def2.
+
+Definition unit_type {T : Type} (x : T) : Prop := forall y : T, y = x.
+Definition is_unit_type (T : Type) : Prop := exists x : T, unit_type x.
+
+End Subset_Def2.
+
+
+Section Subset_Facts.
+
+Context {T : Type}.
+Variable A : T -> Prop.
 
 Lemma is_singleton_equiv :
-  forall {U : Type} (A : U -> Prop) x,
-    A = singleton x <-> nonempty A /\ forall y, A y -> y = x.
+  forall x, A = singleton x <-> nonempty A /\ forall y, A y -> y = x.
 Proof.
-intros U A x; split.
-intros; subst; split; try exists x; easy.
-intros [[y Hy] HA]; apply subset_ext_equiv; split; intros z Hz.
-apply HA; easy.
-rewrite Hz -(HA y); easy.
+intros x; split; [intros; subst; split; [exists x |]; easy |].
+intros [[y Hy] HA]; apply subset_ext_equiv; split; intros z Hz;
+    [apply HA | rewrite Hz -(HA y)]; easy.
 Qed.
 
-Lemma unit_subset_dec :
-  forall {U : Type} (A : U -> Prop) (x : U),
-    unit_type x -> { empty A } + { A = singleton x }.
+Context {x : T}.
+Hypothesis HT : unit_type x.
+
+Lemma unit_subset_dec : { empty A } + { A = singleton x }.
 Proof.
-intros U A x HU.
-destruct (excluded_middle_informative (empty A)) as [HA | HA].
-left; easy.
-right; apply is_singleton_equiv; split.
-apply nonempty_is_not_empty; easy.
-intros; apply HU.
+destruct (empty_dec A) as [HA | HA]; [left; easy |].
+right; apply is_singleton_equiv; split; [easy | intros; apply HT].
 Qed.
 
-Lemma unit_nonempty_subset_is_singleton :
-  forall {U : Type} (A : U -> Prop) (x : U),
-    unit_type x -> nonempty A -> A = singleton x.
+Lemma unit_subset_is_singleton : nonempty A -> A = singleton x.
 Proof.
-intros U A x HU HA.
-destruct (unit_subset_dec A _ HU) as [HA' | HA']; try easy.
-contradict HA'; apply nonempty_is_not_empty; easy.
+intros HA; destruct unit_subset_dec as [HA' |];
+    [contradict HA'; apply nonempty_is_not_empty |]; easy.
 Qed.
 
-Lemma full_fullset_alt : forall {U : Type}, full (@fullset U).
+End Subset_Facts.
+
+
+Section Subset_operator_Facts.
+
+Context {T : Type}.
+
+Lemma full_fullset_alt : full (@fullset T).
 Proof. easy. Qed.
 
-Lemma inter_empty_l :
-  forall {U : Type} (A B : U -> Prop), empty A -> empty (inter A B).
+Lemma inter_empty_l : forall {A} (B : T -> Prop), empty A -> empty (inter A B).
 Proof. move=>> H x Hx; apply (H x), Hx. Qed.
 
-Lemma inter_empty_r :
-  forall {U : Type} (A B : U -> Prop), empty B -> empty (inter A B).
+Lemma inter_empty_r : forall (A : T -> Prop) {B}, empty B -> empty (inter A B).
 Proof. move=>> H x Hx; apply (H x), Hx. Qed.
 
 Lemma union_inj_l :
-  forall {U : Type} (B : U -> Prop) { A1 A2},
+  forall (B : T -> Prop) {A1 A2},
     incl B (compl A1) -> incl B (compl A2) ->
     union A1 B = union A2 B -> A1 = A2.
 Proof.
-intros U B A1 A2 HA1 HA2 HA; apply subset_ext_equiv; split; intros x Hx.
-assert (H1 : union A1 B x) by now left.
-rewrite HA in H1; destruct H1 as [H1 | H1]; [| apply HA1 in H1]; easy.
-assert (H2 : union A2 B x) by now left.
-rewrite -HA in H2; destruct H2 as [H2 | H2]; [| apply HA2 in H2]; easy.
+intros B A1 A2 HA1 HA2 HA; apply subset_ext_equiv; split; intros x Hx.
+move: (union_ub_l A1 B x Hx); rewrite HA; move=> [| /HA1]; easy.
+move: (union_ub_l A2 B x Hx); rewrite -HA; move=> [| /HA2]; easy.
 Qed.
 
 Lemma union_inj_r :
-  forall {U : Type} (A : U -> Prop) {B1 B2},
+  forall (A : T -> Prop) {B1 B2},
     incl A (compl B1) -> incl A (compl B2) ->
     union A B1 = union A B2 -> B1 = B2.
-Proof. intros U A B1 B2; rewrite !(union_comm A); apply union_inj_l. Qed.
+Proof. intros A B1 B2; rewrite !(union_comm A); apply union_inj_l. Qed.
 
 Lemma inter_inj_l :
-  forall {U : Type} (B : U -> Prop ){A1 A2},
+  forall (B : T -> Prop ){A1 A2},
     incl A1 B -> incl A2 B ->
     inter (compl A1) B = inter (compl A2) B -> A1 = A2.
 Proof.
-move=> U B A1 A2 /compl_monot HA1 /compl_monot HA2 /(f_equal compl).
+move=> B A1 A2 /compl_monot HA1 /compl_monot HA2 /(f_equal compl).
 rewrite !compl_inter !compl_invol; intros HA.
 apply compl_reg; rewrite (union_inj_l _ HA1 HA2 HA); easy.
 Qed.
 
 Lemma inter_inj_r :
-  forall {U : Type} (A : U -> Prop) {B1 B2},
+  forall (A : T -> Prop) {B1 B2},
     incl B1 A -> incl B2 A ->
     inter A (compl B1) = inter A (compl B2) -> B1 = B2.
-Proof. intros U A B1 B2; rewrite !(inter_comm A); apply inter_inj_l. Qed.
+Proof. intros A B1 B2; rewrite !(inter_comm A); apply inter_inj_l. Qed.
 
-End Subset_Facts.
+End Subset_operator_Facts.
 
 
 Section Subset_charac_Facts.
 
-Context {U : Type}. (* Universe. *)
+Context {T : Type}.
 
-Lemma charac_inj : injective (@charac U).
+Lemma charac_inj : injective (@charac T).
 Proof.
-move=>> H; apply subset_ext_equiv; split; move=>> Hx; apply charac_1.
-rewrite -H; apply charac_is_1; easy.
-rewrite H; apply charac_is_1; easy.
+move=>> H; apply subset_ext_equiv; split; move=>> Hx; apply charac_1;
+    [rewrite -H | rewrite H]; apply charac_is_1; easy.
 Qed.
 
 End Subset_charac_Facts.
diff --git a/FEM/Compl/logic_compl.v b/FEM/Compl/logic_compl.v
index e30b392e0032c0443cbc016ed038734836f2fb2c..4fceb6835e425e5a91af3836cf952186124fe86b 100644
--- a/FEM/Compl/logic_compl.v
+++ b/FEM/Compl/logic_compl.v
@@ -14,10 +14,40 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-From Coq Require Import Classical.
+(* We need classical logic, and a constructive form of indefinite description. *)
+From Coq Require Import Classical IndefiniteDescription.
 
 
-Section Logic_Facts1.
+(** Additional definitions and results about classical logic.
+
+  'neq' is the "not eq" binary relation on any type.
+  'br_not R' is the negation of any binary relation R on any type.
+
+  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;
+  - all de Morgan's laws for quantifiers.
+
+  ex_EX is an alias for constructive_indefinite_description, where "ex" and "EX"
+  stand for weak existential and strong existential respectively.
+*)
+
+
+Section Logic_Def.
+
+Context {T : Type}.
+
+Definition neq : T -> T -> Prop := fun x y => x <> y.
+
+Variable R : T -> T -> Prop.
+
+(* Prefix br_ stands for binary relation. *)
+Definition br_not : T -> T -> Prop := fun x y => ~ R x y.
+
+End Logic_Def.
+
+
+Section Classical_propositional_Facts1.
 
 Lemma PNNP : forall {P : Prop}, P -> ~ ~ P.
 Proof. tauto. Qed.
@@ -25,10 +55,10 @@ Proof. tauto. Qed.
 Lemma NNPP_equiv : forall (P : Prop), ~ ~ P <-> P.
 Proof. intros; tauto. Qed.
 
-End Logic_Facts1.
+End Classical_propositional_Facts1.
 
 
-Section Logic_Facts2.
+Section Classical_propositional_Facts2.
 
 Context {P Q : Prop}.
 
@@ -65,13 +95,16 @@ Proof. tauto. Qed.
 Lemma iff_not_equiv : (P <-> Q) <-> (~ P <-> ~ Q).
 Proof. tauto. Qed.
 
+Lemma iff_not_l_equiv : (~ P <-> Q) <-> (P <-> ~ Q).
+Proof. tauto. Qed.
+
 Lemma iff_not_r_equiv : (P <-> ~ Q) <-> (~ P <-> Q).
 Proof. tauto. Qed.
 
-End Logic_Facts2.
+End Classical_propositional_Facts2.
 
 
-Section Logic_Facts3.
+Section Classical_propositional_Facts3.
 
 Variable P Q R : Prop.
 
@@ -105,10 +138,10 @@ Proof. tauto. Qed.
 Lemma contra3_not_r_equiv : (P -> Q -> ~ R) <-> (R /\ Q -> ~ P).
 Proof. tauto. Qed.
 
-End Logic_Facts3.
+End Classical_propositional_Facts3.
 
 
-Section Logic_Facts4.
+Section Classical_propositional_Facts4.
 
 Variable P Q R S : Prop.
 
@@ -118,60 +151,46 @@ Proof. tauto. Qed.
 Lemma not_or4_equiv : ~ (P \/ Q \/ R \/ S) <-> ~ P /\ ~ Q /\ ~ R /\ ~ S.
 Proof. tauto. Qed.
 
-End Logic_Facts4.
+End Classical_propositional_Facts4.
 
 
-Section Logic_Facts5.
+Section Classical_propositional_Facts5.
 
-Lemma eq_sym_refl :
-  forall {U : Type} (x : U), eq_sym (@eq_refl _ x) = @eq_refl _ x.
+Context {T : Type}.
+Variable x y : T.
+
+Lemma eq_sym_refl : eq_sym (@eq_refl _ x) = @eq_refl _ x.
 Proof. easy. Qed.
 
-Lemma not_eq_sym_invol :
-  forall {U : Type} {x y : U} (H : x <> y), not_eq_sym (not_eq_sym H) = H.
+Lemma neq_sym_invol : forall (H : x <> y), not_eq_sym (not_eq_sym H) = H.
 Proof. intros; apply proof_irrelevance. Qed.
 
-End Logic_Facts5.
-
-
-Section Logic_Facts6.
-
-Lemma all_and_equiv :
-  forall {U : Type} (P Q : U -> Prop),
-    (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).
-Proof.
-intros; split; intros H; [split; intros | intros; split]; apply H.
-Qed.
-
-Lemma not_all_not_ex_equiv :
- forall {U : Type} (P : U -> Prop), ~ (forall x, ~ P x) <-> exists x, P x.
-Proof.
-intros; split. apply not_all_not_ex. intros [x Hx] H; apply (H x); easy.
-Qed.
+End Classical_propositional_Facts5.
 
-Lemma not_all_ex_not_equiv :
-  forall {U : Type} (P : U -> Prop), ~ (forall x, P x) <-> exists x, ~ P x.
-Proof. intros; split. apply not_all_ex_not. apply ex_not_not_all. Qed.
 
-Lemma not_ex_all_not_equiv :
-  forall {U : Type} (P : U -> Prop), ~ (exists x, P x) <-> forall x, ~ P x.
-Proof. intros; split. apply not_ex_all_not. apply all_not_not_ex. Qed.
+Section Classical_predicate_Facts.
 
-Lemma not_ex_not_all_equiv :
-  forall {U : Type} (P : U -> Prop), ~ (exists x, ~ P x) <-> forall x, P x.
-Proof. intros; split. apply not_ex_not_all. intros H [x Hx]; auto. Qed.
+Context {T : Type}.
+Variable P Q : T -> Prop.
 
-End Logic_Facts6.
+Lemma all_and_equiv :
+  (forall x, P x /\ Q x) <-> (forall x, P x) /\ (forall x, Q x).
+Proof. split; intros H; [split; intros | intros; split]; apply H. Qed.
 
+Lemma not_all_not_ex_equiv : ~ (forall x, ~ P x) <-> exists x, P x.
+Proof. split; [apply not_all_not_ex | intros [x Hx] H; apply (H x); easy]. Qed.
 
-Section Logic_Def.
+Lemma not_all_ex_not_equiv : ~ (forall x, P x) <-> exists x, ~ P x.
+Proof. split; [apply not_all_ex_not | apply ex_not_not_all]. Qed.
 
-Context {T : Type}.
+Lemma not_ex_all_not_equiv : ~ (exists x, P x) <-> forall x, ~ P x.
+Proof. split; [apply not_ex_all_not | apply all_not_not_ex]. Qed.
 
-Definition neq : T -> T -> Prop := fun x y => x <> y.
+Lemma not_ex_not_all_equiv : ~ (exists x, ~ P x) <-> forall x, P x.
+Proof. split; [apply not_ex_not_all | intros H [x Hx]; auto]. Qed.
 
-Variable R : T -> T -> Prop.
-
-Definition br_not : T -> T -> Prop := fun x y => ~ R x y.
+Lemma ex_EX :
+  forall {T : Type} (P : T -> Prop), (exists x, P x) -> { x : T | P x }.
+Proof. exact constructive_indefinite_description. Qed.
 
-End Logic_Def.
+End Classical_predicate_Facts.