diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 53423818e5c582c52d2c76ea0a05dad763dd7024..3b93cd8642debf584e9e5d3929d98b51e9159861 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -16,8 +16,11 @@ COPYING file for more details.
 
 (** Operations on subsets (definitions and properties).
 
-  Subsets of the type U are represented by their belonging function,
-  of type U -> Prop.
+  Subsets of the type U can be defined using predicates: they are represented
+  by belonging functions of type U -> Prop. This is the main API of the file.
+
+  Subsets can also be defined as the range of some function: given some index
+  type Idx, they are represented by "enumerating functions" of type Idx -> U.
 
   Most of the properties are tautologies, and can be found on Wikipedia:
   https://en.wikipedia.org/wiki/List_of_set_identities_and_relations *)
@@ -26,6 +29,23 @@ From Coq Require Import Classical.
 From Coq Require Import PropExtensionality FunctionalExtensionality.
 
 
+Section Base_Def0.
+
+Context {U : Type}. (* Universe. *)
+
+Variable A : U -> Prop. (* Subset throuh predicate. *)
+
+Definition subset_to_Idx : {x | A x} -> U := proj1_sig (P := A).
+
+Context {Idx : Type}. (* Set? *) (* Indices. *)
+
+Variable B : Idx -> U. (* Subset through access to elements. *)
+
+Definition subset_of_Idx : U -> Prop := fun x => exists i, x = B i.
+
+End Base_Def0.
+
+
 Section Base_Def1.
 
 Context {U : Type}. (* Universe. *)
@@ -132,37 +152,47 @@ Definition swap : forall {U : Type}, (U1 * U2 -> U) -> U2 * U1 -> U :=
 End Base_Def4.
 
 
-Section Base_Def5.
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f g : U1 -> U2. (* Function. *)
-
-Definition same_fun : Prop := forall x, f x = g x.
-
-Variable A1 : U1 -> Prop. (* Subset. *)
-Variable A2 : U2 -> Prop. (* Subset. *)
-
-Inductive image : U2 -> Prop := Im : forall x1, A1 x1 -> image (f x1).
-
-Definition image_ex : U2 -> Prop :=
-  fun x2 => exists x1, A1 x1 /\ x2 = f x1.
+Section Prop_Facts0.
 
-Definition preimage : U1 -> Prop := fun x1 => A2 (f x1).
+Context {U : Type}. (* Universe. *)
 
-Context {U3 : Type}. (* Universe. *)
+(** Correctness results. *)
 
-Variable f23 : U2 -> U3. (* Function. *)
-Variable f12 : U1 -> U2. (* Function. *)
+Lemma subset_to_Idx_correct :
+  forall (A : U -> Prop) x, A x <-> exists i, x = subset_to_Idx A i.
+Proof.
+intros A x; split.
+intros Hx; exists (exist _ x Hx); easy.
+intros [[y Hy] Hx]; rewrite Hx; easy.
+Qed.
 
-Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).
+Context {Idx : Type}. (* Indices. *)
 
-End Base_Def5.
+(* Useless?
+Lemma subset_of_Idx_correct :
+  forall B (x : U), (exists (i : Idx), x = B i) <-> subset_of_Idx B x.
+Proof.
+tauto.
+Qed.
+*)
 
+Lemma subset_of_Idx_to_Idx :
+  forall (A : U -> Prop) x, subset_of_Idx (subset_to_Idx A) x <-> A x.
+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! *)
 
-Section Prop_Facts0.
+Admitted.
 
-Context {U : Type}. (* Universe. *)
+(* 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.
+Proof.
+Admitted.
+*)
 
 (** Extensionality of subsets. *)
 
@@ -189,8 +219,8 @@ End Prop_Facts0.
 
 Ltac subset_unfold :=
   repeat unfold
-    same_fun, partition, disj, same, incl, full, nonempty, empty, (* Predicates. *)
-    compose, preimage, pair, (* Constructors. *)
+    partition, disj, same, incl, full, nonempty, empty, (* Predicates. *)
+    pair, (* Constructors. *)
     swap, prod, sym_diff, diff, add, inter, union, compl, (* Operators. *)
     singleton, Prop_cst, fullset, emptyset. (* Constructors. *)
 
@@ -396,35 +426,6 @@ apply empty_emptyset; intros x Hx; apply (H2 x); auto.
 now rewrite H2.
 Qed.
 
-(** Facts about same_fun. *)
-
-(** It is an equivalence binary relation. *)
-
-Context {V : Type}. (* Universe. *)
-
-(* Useless?
-Lemma same_fun_refl :
-  forall (f : U -> V),
-    same_fun f f.
-Proof.
-easy.
-Qed.*)
-
-(* Useful? *)
-Lemma same_fun_sym :
-  forall (f g : U -> V),
-    same_fun f g -> same_fun g f.
-Proof.
-easy.
-Qed.
-
-Lemma same_fun_trans :
-  forall (f g h : U -> V),
-    same_fun f g -> same_fun g h -> same_fun f h.
-Proof.
-intros f g h H1 H2 x; now rewrite (H1 x).
-Qed.
-
 End Prop_Facts.
 
 
@@ -559,7 +560,7 @@ Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma empty_union :
+Lemma union_empty :
   forall (A B : U -> Prop),
     union A B = emptyset <-> A = emptyset /\ B = emptyset.
 Proof.
@@ -726,7 +727,7 @@ Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma full_inter :
+Lemma inter_full :
   forall (A B : U -> Prop),
     inter A B = fullset <-> A = fullset /\ B = fullset.
 Proof.
@@ -972,7 +973,7 @@ intros A B H1 H2 H3; rewrite disj_equiv_def in H1, H3.
 contradict H2; apply empty_emptyset.
 rewrite <- (inter_full_l B).
 rewrite <- (union_compl_l A), inter_union_distr_r, H1, H3.
-now apply empty_union.
+now apply union_empty.
 Qed.
 
 Lemma disj_compl_r :
@@ -1835,263 +1836,3 @@ intros; subset_ext_auto.
 Qed.
 
 End Prod_Facts.
-
-
-Section Image_Facts.
-
-(** Facts about images. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f g : U1 -> U2. (* Functions. *)
-
-Lemma image_eq : forall A1, image f A1 = image_ex f A1.
-Proof.
-intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1].
-exists x1; easy.
-rewrite (proj2 Hx1); easy.
-Qed.
-
-Lemma image_ext_fun : forall A1, same_fun f g -> image f A1 = image g A1.
-Proof.
-intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1];
-    [rewrite H | rewrite <- H]; easy.
-Qed.
-
-Lemma image_ext : forall A1 B1, same A1 B1 -> image f A1 = image f B1.
-Proof.
-intros A1 B1 H.
-subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1]; apply Im; apply H; easy.
-Qed.
-
-Lemma image_empty_equiv :
-  forall A1, empty (image f A1) <-> empty A1.
-Proof.
-intros A1; split; intros HA1.
-intros x1 Hx1; apply (HA1 (f x1)); easy.
-intros x2 [x1 Hx1]; apply (HA1 x1); easy.
-Qed.
-
-Lemma image_emptyset : image f emptyset = emptyset.
-Proof.
-apply empty_emptyset, image_empty_equiv; easy.
-Qed.
-
-Lemma image_monot :
-  forall A1 B1, incl A1 B1 -> incl (image f A1) (image f B1).
-Proof.
-intros A1 B1 H1 x2 [x1 Hx1]; apply Im, H1; easy.
-Qed.
-
-Lemma image_union :
-  forall A1 B1, image f (union A1 B1) = union (image f A1) (image f B1).
-Proof.
-intros A1 B1; apply subset_ext_equiv; split; intros x2.
-intros [x1 [Hx1 | Hx1]]; [left | right]; easy.
-intros [[x1 Hx1] | [x1 Hx1]]; apply Im; [left | right]; easy.
-Qed.
-
-Lemma image_inter :
-  forall A1 B1, incl (image f (inter A1 B1)) (inter (image f A1) (image f B1)).
-Proof.
-intros A1 B1 x2 [x1 Hx1]; split; apply Im, Hx1.
-Qed.
-
-Lemma image_diff :
-  forall A1 B1, incl (diff (image f A1) (image f B1)) (image f (diff A1 B1)).
-Proof.
-intros A1 B1 x2 [[x1 Hx1] Hx2']; apply Im; split; try easy.
-intros Hx1'; apply Hx2'; easy.
-Qed.
-
-Lemma image_compl : forall A1, incl (diff (image f fullset) (image f A1)) (image f (compl A1)).
-Proof.
-intros; rewrite compl_equiv_def_diff; apply image_diff.
-Qed.
-
-Lemma image_sym_diff :
-  forall A1 B1,
-    incl (sym_diff (image f A1) (image f B1)) (image f (sym_diff A1 B1)).
-Proof.
-intros; unfold sym_diff; rewrite image_union.
-apply union_monot; apply image_diff.
-Qed.
-
-End Image_Facts.
-
-
-Section Preimage_Facts.
-
-(** Facts about preimages. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f g : U1 -> U2. (* Functions. *)
-
-Lemma preimage_ext_fun :
-  forall A2, same_fun f g -> preimage f A2 = preimage g A2.
-Proof.
-intros A2 H; subset_ext_auto x1; rewrite (H x1); easy.
-Qed.
-
-Lemma preimage_ext :
-  forall A2 B2, same A2 B2 -> preimage f A2 = preimage f B2.
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_empty_equiv :
-  forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
-Proof.
-intros A2; split.
-intros HA2 x2 Hx2a Hx2b; induction Hx2b as [x1 Hx1]; apply (HA2 x1); easy.
-intros HA2 x1 Hx1; apply (HA2 (f x1)); easy.
-Qed.
-
-Lemma preimage_emptyset : preimage f emptyset = emptyset.
-Proof.
-apply empty_emptyset, preimage_empty_equiv; easy.
-Qed.
-
-Lemma preimage_full_equiv :
-  forall A2, full (preimage f A2) <-> incl (image f fullset) A2.
-Proof.
-intros A2; split; intros HA2.
-intros x2 [x1 Hx1]; apply HA2.
-intros x1; apply HA2; easy.
-Qed.
-
-Lemma preimage_monot :
-  forall A2 B2, incl A2 B2 -> incl (preimage f A2) (preimage f B2).
-Proof.
-intros; subset_auto.
-Qed.
-
-Lemma preimage_compl :
-  forall A2, preimage f (compl A2) = compl (preimage f A2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_union :
-  forall A2 B2,
-    preimage f (union A2 B2) = union (preimage f A2) (preimage f B2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_inter :
-  forall A2 B2,
-    preimage f (inter A2 B2) = inter (preimage f A2) (preimage f B2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_diff :
-  forall A2 B2,
-    preimage f (diff A2 B2) = diff (preimage f A2) (preimage f B2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_sym_diff :
-  forall A2 B2,
-    preimage f (sym_diff A2 B2) = sym_diff (preimage f A2) (preimage f B2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_cst :
-  forall A2 (x2 : U2), preimage (fun _ : U1 => x2) A2 = Prop_cst (A2 x2).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-End Preimage_Facts.
-
-
-Section Image_Preimage_Facts.
-
-(** Facts about images and preimages. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f : U1 -> U2. (* Function. *)
-
-Lemma image_of_preimage :
-  forall A2, image f (preimage f A2) = inter A2 (image f fullset).
-Proof.
-intros A2; apply subset_ext; intros x2; split.
-intros Hx2; induction Hx2 as [x1 Hx1]; easy.
-intros [Hx2 Hx2']; induction Hx2' as [x1 Hx1]; easy.
-Qed.
-
-Lemma image_of_preimage_of_image :
-  forall A1, image f (preimage f (image f A1)) = image f A1.
-Proof.
-intros; rewrite image_of_preimage; apply inter_left, image_monot; easy.
-Qed.
-
-Lemma preimage_of_image : forall A1, incl A1 (preimage f (image f A1)).
-Proof.
-easy.
-Qed.
-
-Lemma preimage_of_image_full : preimage f (image f fullset) = fullset.
-Proof.
-apply subset_ext_equiv; easy.
-Qed.
-
-Lemma preimage_of_image_of_preimage :
-  forall A2, preimage f (image f (preimage f A2)) = preimage f A2.
-Proof.
-intros; rewrite image_of_preimage.
-rewrite preimage_inter, preimage_of_image_full.
-apply inter_full_r.
-Qed.
-
-Lemma preimage_of_image_equiv :
-  forall A1, (preimage f (image f A1)) = A1 <-> exists A2, preimage f A2 = A1.
-Proof.
-intros A1; split.
-intros HA1; exists (image f A1); easy.
-intros [A2 HA2]; rewrite <- HA2; apply preimage_of_image_of_preimage.
-Qed.
-
-End Image_Preimage_Facts.
-
-
-Section Compose_Facts.
-
-(** Facts about composition of functions. *)
-
-Context {U1 U2 U3 U4 : Type}. (* Universes. *)
-
-Variable f12 : U1 -> U2. (* Function. *)
-Variable f23 : U2 -> U3. (* Function. *)
-Variable f34 : U3 -> U4. (* Function. *)
-
-(* Useful? *)
-Lemma compose_assoc :
-  compose f34 (compose f23 f12) = compose (compose f34 f23) f12.
-Proof.
-easy.
-Qed.
-
-Lemma image_compose :
-  forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
-Proof.
-intros A1; apply subset_ext_equiv; split; intros x3 Hx3.
-induction Hx3 as [x1 Hx1]; easy.
-induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
-replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
-Qed.
-
-(* Useful? *)
-Lemma preimage_compose :
-  forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
-Proof.
-easy.
-Qed.
-
-End Compose_Facts.
diff --git a/Lebesgue/Subset_finite.v b/Lebesgue/Subset_finite.v
index 1d632a7380ee89981f59fd6ba48293d6192663a7..676b52d45b9da8cf6c51d4d4b199a46328f55d84 100644
--- a/Lebesgue/Subset_finite.v
+++ b/Lebesgue/Subset_finite.v
@@ -18,12 +18,12 @@ COPYING file for more details.
 
   Subsets of type U are represented by functions of type U -> Prop.
 
-  Most identities can be found on Wikipedia:
+  Most of the properties are tautologies, and can be found on Wikipedia:
   https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
 
-  All or parts of this file could use results on BigOps from MathComp. *)
+  All or parts of this file could use BigOps from MathComp. *)
 
-From Coq Require Import ClassicalChoice (*ChoiceFacts*).
+From Coq Require Import ClassicalChoice.
 From Coq Require Import FunctionalExtensionality.
 From Coq Require Import Arith Lia.
 
@@ -116,7 +116,7 @@ Definition incl_finite : Prop :=
   forall n, n < S N -> incl (A n) (B n).
 
 Definition same_finite : Prop :=
-  forall n, n < S N -> same (A n) (B n).
+  forall n, n < S N -> same (A n) (B n). (* Should it be A n = B n? *)
 
 (* Warning: incr actually means nondecreasing. *)
 Definition incr_finite : Prop :=
@@ -209,7 +209,8 @@ End Finite_Facts0.
 
 
 Ltac subset_finite_unfold :=
-  repeat unfold partition_finite, disj_finite_alt, disj_finite,
+  repeat unfold
+    partition_finite, disj_finite_alt, disj_finite,
       decr_finite, incr_finite, same_finite, incl_finite, (* Predicates. *)
     prod_finite_r, prod_finite_l, inter_finite, union_finite,
       x_diff_finite, x_inter_finite, compl_finite,
@@ -219,7 +220,7 @@ Ltac subset_finite_full_unfold :=
   subset_finite_unfold; subset_unfold.
 
 Ltac subset_finite_auto :=
-  subset_finite_unfold; try easy; try tauto.
+  subset_finite_unfold; try easy; try tauto; auto.
 
 Ltac subset_finite_full_auto :=
   subset_finite_unfold; subset_auto.
@@ -719,7 +720,7 @@ intros [N2 [HN2 [n [Hn Hx]]]]; exists n; split; [lia | easy].
 intros Hx; exists N1; split; [lia | easy].
 Qed.
 
-Lemma empty_union_finite :
+Lemma union_finite_empty :
   forall (A : nat -> U -> Prop) N,
     union_finite A N = emptyset <->
     forall n, n < S N -> A n = emptyset.
@@ -971,7 +972,7 @@ intros Hx n Hn; apply (Hx N1); [lia | easy].
 intros Hx N2 HN2 n Hn; apply Hx; lia.
 Qed.
 
-Lemma full_inter_finite :
+Lemma inter_finite_full :
   forall (A : nat -> U -> Prop) N,
     inter_finite A N = fullset <->
     forall n, n < S N -> A n = fullset.
@@ -1409,56 +1410,3 @@ intros HA; split; now try apply HA.
 Qed.
 
 End Prod_Facts.
-
-
-Section Image_Facts.
-
-(** Facts about images. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f : U1 -> U2. (* Function. *)
-
-Lemma image_union_finite_distr :
-  forall A1 N,
-    image f (union_finite A1 N) = union_finite (fun n => image f (A1 n)) N.
-Proof.
-intros A1 N; apply subset_ext_equiv; split; intros x2.
-intros [x1 [n [Hn Hx1]]]; exists n; split; easy.
-intros [n [Hn [x1 Hx1]]]; apply Im; exists n; easy.
-Qed.
-
-Lemma image_inter_finite :
-  forall A1 N,
-    incl (image f (inter_finite A1 N))
-      (inter_finite (fun n => image f (A1 n)) N).
-Proof.
-intros A1 N x2 [x1 Hx1] n Hn; apply Im, Hx1; easy.
-Qed.
-
-End Image_Facts.
-
-
-Section Preimage_Facts.
-
-(** Facts about preimages. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f : U1 -> U2. (* Function. *)
-
-Lemma preimage_union_finite_distr :
-  forall A2 N,
-    preimage f (union_finite A2 N) = union_finite (fun n => preimage f (A2 n)) N.
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_inter_finite_distr :
-  forall A2 N,
-    preimage f (inter_finite A2 N) = inter_finite (fun n => preimage f (A2 n)) N.
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-End Preimage_Facts.
diff --git a/Lebesgue/Subset_seq.v b/Lebesgue/Subset_seq.v
index 091527bb1ab8a90317f1ae31ee74b49a30906235..f08180a91e647816f075ced44db529ee1f95df3f 100644
--- a/Lebesgue/Subset_seq.v
+++ b/Lebesgue/Subset_seq.v
@@ -18,10 +18,10 @@ COPYING file for more details.
 
   Subsets of type U are represented by functions of type U -> Prop.
 
-  Most identities can be found on Wikipedia:
+  Most of the properties are tautologies, and can be found on Wikipedia:
   https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
 
-  All or parts of this file could use results on BigOps from MathComp. *)
+  All or parts of this file could use BigOps from MathComp. *)
 
 From Coq Require Import Classical FunctionalExtensionality FinFun.
 From Coq Require Import Arith Lia Even.
@@ -56,7 +56,7 @@ Definition incl_seq : Prop :=
   forall n, incl (A n) (B n).
 
 Definition same_seq : Prop :=
-  forall n, same (A n) (B n). (* Should be A n = B n ? *)
+  forall n, same (A n) (B n). (* Should it be A n = B n? *)
 
 (* Warning: incr actually means nondecreasing. *)
 Definition incr_seq : Prop :=
@@ -142,7 +142,8 @@ End Seq_Facts0.
 
 
 Ltac subset_seq_unfold :=
-  repeat unfold partition_seq, disj_seq_alt, disj_seq,
+  repeat unfold
+    partition_seq, disj_seq_alt, disj_seq,
       decr_seq, incr_seq, same_seq, incl_seq, (* Predicates. *)
     prod_seq_r, prod_seq_l, inter_seq, union_seq,
       x_inter_seq, compl_seq. (* Operators. *)
@@ -151,7 +152,7 @@ Ltac subset_seq_full_unfold :=
   subset_seq_unfold; subset_finite_full_unfold.
 
 Ltac subset_seq_auto :=
-  subset_seq_unfold; try easy; try tauto.
+  subset_seq_unfold; try easy; try tauto; auto.
 
 Ltac subset_seq_full_auto :=
   subset_seq_unfold; subset_finite_full_auto.
@@ -643,7 +644,7 @@ intros [N [n [_ Hx]]]; now exists n.
 intros [n Hx]; exists (S n), n; split; [lia | easy].
 Qed.
 
-Lemma empty_union_seq :
+Lemma union_seq_empty :
   forall (A : nat -> U -> Prop),
     union_seq A = emptyset <-> forall n, A n = emptyset.
 Proof.
@@ -829,7 +830,7 @@ intros H n; apply (H (S n) n); lia.
 intros H N n _; apply H.
 Qed.
 
-Lemma full_inter_seq :
+Lemma inter_seq_full :
   forall (A : nat -> U -> Prop),
     inter_seq A = fullset <-> forall n, A n = fullset.
 Proof.
@@ -1209,57 +1210,6 @@ Qed.
 End Prod_Facts.
 
 
-Section Image_Facts.
-
-(** Facts about images. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f : U1 -> U2. (* Function. *)
-
-Lemma image_union_seq_distr :
-  forall A1, image f (union_seq A1) = union_seq (fun n => image f (A1 n)).
-Proof.
-intros A1; apply subset_ext_equiv; split; intros x2.
-intros [x1 [n Hx1]]; exists n; easy.
-intros [n [x1 Hx1]]; apply Im; exists n; easy.
-Qed.
-
-Lemma image_inter_seq :
-  forall A1,
-    incl (image f (inter_seq A1)) (inter_seq (fun n => image f (A1 n))).
-Proof.
-intros A1 x2 [x1 Hx1] n; apply Im, Hx1.
-Qed.
-
-End Image_Facts.
-
-
-Section Preimage_Facts.
-
-(** Facts about preimages. *)
-
-Context {U1 U2 : Type}. (* Universes. *)
-
-Variable f : U1 -> U2. (* Function. *)
-
-Lemma preimage_union_seq_distr :
-  forall A2,
-    preimage f (union_seq A2) = union_seq (fun n => preimage f (A2 n)).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-Lemma preimage_inter_seq_distr :
-  forall A2,
-    preimage f (inter_seq A2) = inter_seq (fun n => preimage f (A2 n)).
-Proof.
-intros; subset_ext_auto.
-Qed.
-
-End Preimage_Facts.
-
-
 Section Limit_Def.
 
 Context {U : Type}. (* Universe. *)