diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 3b93cd8642debf584e9e5d3929d98b51e9159861..ef4a1583f99d2d02d5e9a74b524e7e50ca3b4a0f 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -181,17 +181,14 @@ Lemma subset_of_Idx_to_Idx :
 Proof.
 intros A x; split.
 intros [[y Hy] Hi]; rewrite Hi; easy.
-intros Hx.
-assert (i : {x | A x}) by now exists x.
-exists i. (* Pb: i is no longer bound to x! *)
-
-Admitted.
+intros Hx; exists (exist _ _ Hx); easy.
+Qed.
 
 (* WIP: this one is not typing yet!
 Lemma subset_to_Idx_of_Idx :
-  forall Idx (B : Idx -> U) i, subset_to_Idx (subset_of_Idx B) i = B i.
+  forall Idx (B : Idx -> U) (i : Idx), subset_to_Idx (subset_of_Idx B) i = B i.
 Proof.
-Admitted.
+Aglopted.
 *)
 
 (** Extensionality of subsets. *)
diff --git a/Lebesgue/Subset_system.v b/Lebesgue/Subset_system.v
index 32f1e691de4b528a67039404a6491b601795c50d..68405801d26ba4c896b61907d2198d86d2996353 100644
--- a/Lebesgue/Subset_system.v
+++ b/Lebesgue/Subset_system.v
@@ -2463,17 +2463,15 @@ Section equiv_SA.
 Context {E : Type}.
 Variable gen : (E -> Prop) -> Prop.
 
-Lemma measurable_Sigma_algebra :
-   forall A, measurable gen A <-> Sigma_algebra gen A.
+Lemma measurable_Sigma_algebra : measurable gen = Sigma_algebra gen.
 Proof.
-intros A; split; intros H.
-induction H.
+apply subset_ext; intro; split; intros H; induction H.
+(* *)
 apply Sigma_algebra_Gen; easy.
 apply Sigma_algebra_wEmpty.
 apply Sigma_algebra_Compl_rev; easy.
 apply Sigma_algebra_Union_seq; easy.
 (* *)
-induction H.
 apply measurable_gen; easy.
 apply measurable_empty.
 apply measurable_compl_rev; easy.
@@ -2481,3 +2479,20 @@ apply measurable_union_countable; easy.
 Qed.
 
 End equiv_SA.
+
+
+Section equiv_GP.
+
+Context {U1 U2 : Type}.
+Variable genU1 : (U1 -> Prop) -> Prop.
+Variable genU2 : (U2 -> Prop) -> Prop.
+
+Lemma Gen_Prod_Gen_Product : Gen_Prod genU1 genU2 = Gen_Product genU1 genU2.
+Proof.
+apply subset_ext; intro; split; intros [A1 [A2 [HA1 [HA2 HA]]]];
+    exists A1, A2; (split; [easy | split; [easy |]]).
+rewrite HA; easy.
+apply subset_ext; easy.
+Qed.
+
+End equiv_GP.
diff --git a/Lebesgue/Subset_system_base.v b/Lebesgue/Subset_system_base.v
index 8ab9a1158dac1d21fb84fcc4df6fcead41922744..7c48e2f953c2a852d62973465bd37f1556202c05 100644
--- a/Lebesgue/Subset_system_base.v
+++ b/Lebesgue/Subset_system_base.v
@@ -443,13 +443,9 @@ Lemma Preimage_compose :
   forall P3, Preimage (compose f23 f12) P3 = Preimage f12 (Preimage f23 P3).
 Proof.
 intros P3; unfold Preimage; subset_ext_auto A1 HA1.
-induction HA1 as [A3 HA3].
-admit.
-
-induction HA1 as [A2 HA2].
-
-
-Admitted.
+destruct HA1 as [A3 HA3]; rewrite preimage_compose; easy.
+destruct HA1 as [A2 [A1 HA1]]. rewrite <- preimage_compose. easy.
+Qed.
 
 End Image_Preimage_Facts2.
 
@@ -1248,34 +1244,36 @@ intros A [B [HB1 [HB2 _]]].
 exists B; now split.
 Qed.
 
+(* Unused.
 Lemma Inter_Union_disj_seq_closure :
   Inter P -> Inter (Union_disj_seq_closure P).
 Proof.
 intros H A A' [B [HB1 HB2]] [B' [HB'1 HB'2]].
-Admitted.
+Aglopted.
 
 Lemma Inter_seq_Union_disj_seq_closure :
   Inter P -> Inter_seq (Union_disj_seq_closure P).
 Proof.
-Admitted.
+Aglopted.
 
 Lemma Union_disj_Union_disj_seq_closure :
   Union_disj (Union_disj_seq_closure P).
 Proof.
 intros A A' H [B [HB1 HB2]] [B' [HB'1 HB'2]].
 (* Use mix? *)
-Admitted.
+Aglopted.
 
 Lemma Union_disj_seq_Union_disj_seq_closure :
   Union_disj_seq (Union_disj_seq_closure P).
 Proof.
-Admitted.
+Aglopted.
 
 Lemma Diff_Union_disj_seq_closure :
   Inter P -> Part_diff_seq P -> Diff (Union_disj_seq_closure P).
 Proof.
 intros H1 H2 A A' [B [HB1 [HB2 HB3]]] [B' [HB'1 [HB'2 HB'3]]].
-Admitted.
+Aglopted.
+*)
 
 End Seq_Facts2.
 
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index 07c135e9b760e9d7cb582fc4d89ac3e7385eb345..00bf8e10105b9b189d12a065804f6a00ff5c604f 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -221,31 +221,27 @@ Lemma monotone_class_and_measurable :
     forall A, measurable genX1xX2 A -> Q A.
 Proof.
 intros Q H1 H2 H3 A H4.
-assert (measurable genX1xX2 A /\ Q A).
-2: easy.
+assert (H5 : measurable genX1xX2 A /\ Q A); [| easy].
 apply (monotone_class_Prop (Algebra genX1xX2))
-  with (P:= fun A => measurable genX1xX2 A /\ Q A).
-apply Monotone_class_equiv; try easy.
-split.
+  with (P := fun A => measurable genX1xX2 A /\ Q A).
+(* *)
+apply Monotone_class_equiv; try easy; split.
+(* . *)
 intros B HB H; split.
 apply measurable_inter_countable; intros n; apply H.
-apply H2; try easy.
-intros n; apply H.
-apply H.
+apply H2; try easy; intros n; apply H.
+(* . *)
 split.
-apply measurable_union_countable.
-apply H0.
-apply H3; try easy.
-intros n; apply H0.
-apply H0.
-intros B H; rewrite Algebra_idem in H; split.
-apply measurable_Sigma_algebra.
-apply Incl_Algebra_Sigma_algebra; easy.
-apply H1, Algebra_Gen_Prod_Prod_Sigma_algebra_Incl.
-admit. (* Temporary until Gen_Product from sigma_alebra.v is replaced by Gen_Prod from Subset_system.v. *)
-rewrite Sigma_algebra_Algebra.
-apply measurable_Sigma_algebra; easy.
-Admitted.
+apply measurable_union_countable, H0.
+apply H3; try easy; intros n; apply H0.
+(* *)
+intros B HB; rewrite Algebra_idem in HB; split.
+rewrite measurable_Sigma_algebra; apply Incl_Algebra_Sigma_algebra; easy.
+apply H1, Algebra_Gen_Prod_Prod_Sigma_algebra_Incl;
+    rewrite Gen_Prod_Gen_Product; easy.
+(* *)
+rewrite Sigma_algebra_Algebra, <- measurable_Sigma_algebra; easy.
+Qed.
 
 (* Lemma 827 (1) pp. 175-176 *)
 Lemma meas_section_measurable_finite_aux0 :
@@ -260,7 +256,7 @@ f_equal; apply functional_extensionality; intros x2.
 apply propositional_extensionality; now rewrite H3.
 apply measurable_fun_scal.
 apply measurable_fun_charac.
-now apply measurable_Sigma_algebra.
+rewrite measurable_Sigma_algebra; easy.
 Qed.
 
 (* Lemma 827 (2) pp. 175-176 *)
@@ -624,7 +620,7 @@ Lemma meas_prod_uniqueness_aux0 :
 Proof.
 intros A [A1 [A2 [HA1 [HA2 H]]]].
 rewrite H, Hmu, Hnu; try easy.
-all: now apply measurable_Sigma_algebra.
+all: rewrite measurable_Sigma_algebra; easy.
 Qed.
 
 (* From Lemma 835 (2) pp. 179-180 *)
@@ -639,9 +635,8 @@ rewrite (measure_ext _ nu _ (fun x => exists n, (n <= N)%nat /\ B n x)).
 (* *)
 assert (HB1' : forall n, (n <= N)%nat -> measurable genX1xX2 (B n)).
 intros n Hn; rewrite measurable_Sigma_algebra.
-unfold genX1xX2; admit. (* Temporary. Should be
-rewrite Sigma_algebra_Prod_eq.
-apply Sigma_algebra_Gen, HB1; lia. *)
+unfold genX1xX2; rewrite <- Gen_Prod_Gen_Product, <- Sigma_algebra_Prod_eq.
+apply Sigma_algebra_Gen, HB1; lia.
 (* *)
 assert (HB2' : forall n m x, (n <= N)%nat -> (m <= N)%nat -> B n x -> B m x -> n = m).
 rewrite <- Subset_finite.disj_finite_equiv in HB2.
@@ -649,7 +644,7 @@ intros n m x2 Hn Hm HBn HBm; apply (HB2 n m x2); now try lia.
 (* *)
 rewrite 2!measure_additivity_finite; try easy.
 apply sum_Rbar_ext; intros i Hi; apply meas_prod_uniqueness_aux0, HB1; lia.
-Admitted.
+Qed.
 
 (* From Lemma 835 (3) p. 180 *)
 Lemma meas_prod_uniqueness_aux2 :
@@ -679,7 +674,8 @@ Qed.
 Lemma meas_prod_uniqueness_finite :
   forall A, measurable genX1xX2 A -> mu A = nu A.
 Proof.
-apply monotone_class_and_measurable with muX2; try easy.
+intros A HA; eapply (monotone_class_and_measurable (fun A => mu A = nu A)).
+4: apply HA.
 intros; now apply meas_prod_uniqueness_aux1.
 intros; now apply meas_prod_uniqueness_aux2.
 intros; now apply meas_prod_uniqueness_aux3.
diff --git a/Lebesgue/Topology.v b/Lebesgue/Topology.v
index 67f1b8ddbc3c5279d4b24f91348f08d70aa35b2f..924333adbbfdc96e25e187f06fa6bfa5355e9203 100644
--- a/Lebesgue/Topology.v
+++ b/Lebesgue/Topology.v
@@ -85,6 +85,7 @@ Context {T1 T2 : UniformSpace}.
 
 Variable f : T1 -> T2.
 
+(*
 Lemma topo_basis_compat_is_continuous :
   forall (P2 : (T2 -> Prop) -> Prop),
     is_topo_basis_Prop P2 ->
@@ -97,7 +98,7 @@ intros P2 HP2 Hf x1.
 
 
 
-Admitted.
+Aglopted.
 
 Lemma continuous_equiv_open :
   (forall x1, continuous f x1) <->
@@ -120,6 +121,7 @@ rewrite continuous_equiv_open; split; intros Hf A2 HA2.
 
 
 
-Admitted.
+Aglopted.
+*)
 
 End topo_basis_Facts2.
diff --git a/Lebesgue/UniformSpace_compl.v b/Lebesgue/UniformSpace_compl.v
index 97c34332707713734586aea7f5565e17e7e38d9d..55abf7116a85494f41ac47b9afc9eb8d8f5fe881 100644
--- a/Lebesgue/UniformSpace_compl.v
+++ b/Lebesgue/UniformSpace_compl.v
@@ -262,6 +262,7 @@ intros y [Hy1 Hy2]; split; [apply He1b | apply He2b];
     apply ball_le with e; try easy; [apply Rmin_l | apply Rmin_r].
 Qed.
 
+(*
 Lemma continuous_is_open_compat :
   forall {T1 T2 : UniformSpace} (f : T1 -> T2),
     (forall x1, continuous f x1) ->
@@ -273,7 +274,8 @@ intros T1 T2 f Hf A2 HA2 x1 Hx1.
 
 
 
-Admitted.
+Aglopted.
+*)
 
 End UniformSpace_compl.
 
diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index 1e5b295d2d1b54bf25a7b67a569616c3087166bb..f7dc06b93d8cb60f1c7faf5aceb40b97435c3073 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -283,6 +283,7 @@ Context {E : Type}. (* Universe. *)
 
 Variable P : (E -> Prop) -> Prop. (* Subset system. *)
 
+(*
 Lemma measurable_subspace :
   forall F, is_Sigma_algebra P -> is_Sigma_algebra (Trace P F).
 Proof.
@@ -293,7 +294,8 @@ apply Trace_wEmpty; easy.
 
 
 
-Admitted.
+Aglopted.
+*)
 
 End measurable_subspace.
 
diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v
index f66817a47ff3cecd00e4e278cae27860cdbf0b7d..f817f3eb155b5567e93251f78b747da6e3ee99b4 100644
--- a/Lebesgue/measurable_Rbar.v
+++ b/Lebesgue/measurable_Rbar.v
@@ -234,7 +234,7 @@ Lemma measurable_Rbar_R_alt_incl_lt :
 Proof.
 intros B HB; induction HB as [A HA | A HA | A HA | A HA];
     rewrite measurable_R_eq_lt in HA.
-Admitted.
+Aglopted.
 
 Lemma measurable_Rbar_R_eq_lt :
   measurable_Rbar_R = measurable gen_Rbar_lt.
@@ -242,14 +242,14 @@ Proof.
 apply Ext_equiv; split.
 (* *)
 unfold measurable_Rbar_R; rewrite measurable_R_eq_lt; intros B HB.
-admit.
+aglop.
 (* *)
 apply measurable_gen_lub_alt.
 apply measurable_Rbar_R_is_sigma_algebra.
 intros B HB; induction HB as [a].
 apply measurable_ext with (Rlt a); try easy.
 apply measurable_R_lt.
-Admitted.
+Aglopted.
 
 Lemma measurable_Rbar_Borel_eq_lt :
   measurable_Rbar_Borel = measurable gen_Rbar_lt.
@@ -536,7 +536,7 @@ Qed.
 Lemma measurable_Rbar_abs :
   forall B, measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_abs y)).
 Proof.
-Admitted.
+Aglopted.
 *)
 
 (* WIP [lazy]: wait for actually needin it...
@@ -544,7 +544,7 @@ Lemma measurable_Rbar_scal :
   forall B l,
     measurable_Rbar B -> measurable_Rbar (fun y => B (Rbar_mult l y)).
 Proof.
-Admitted.
+Aglopted.
 *)
 
 End measurable_Rbar.
diff --git a/Lebesgue/measurable_fun_new.v b/Lebesgue/measurable_fun_new.v
index e1b593f277081fa215a92ec73427864c6a96b90b..fd8aa5723333e5fe51da05e708dcf8f22a396306 100644
--- a/Lebesgue/measurable_fun_new.v
+++ b/Lebesgue/measurable_fun_new.v
@@ -119,7 +119,7 @@ Proof.
 intros f12 f23 H12 H23; unfold measurable_fun.
 rewrite Preimage_compose.
 eapply Incl_trans; [apply Preimage_monot, H23 | apply H12].
-Admitted.
+Qed.
 
 End Measurable_fun_Facts1.