Use new Subset_system_def.

Lebesgue/Subset_R.v

@@ -19,7 +19,7 @@ From Coquelicot Require Import Coquelicot.
 
 Require Import R_compl Rbar_compl countable_sets topo_bases_R.
 Require Import Subset Subset_dec Subset_seq.
-Require Import Subset_system_base.
+Require Import Subset_system_def Subset_system_base.
 
 
 Open Scope R_scope.

Lebesgue/Subset_Rbar.v

@@ -20,7 +20,7 @@ From Coquelicot Require Import Coquelicot.
 Require Import nat_compl countable_sets.
 Require Import R_compl Rbar_compl UniformSpace_compl topo_bases_R.
 Require Import Subset Subset_dec Subset_seq.
-Require Import Subset_system_base Subset_R.
+Require Import Subset_system_def Subset_system_base Subset_R.
 
 
 Open Scope R_scope.

Lebesgue/Subset_system.v

@@ -21,8 +21,8 @@ COPYING file for more details.
 From Coq Require Import ClassicalChoice.
 
 Require Import nat_compl.
-Require Import Subset Subset_dec Subset_finite Subset_seq.
-Require Import Subset_system_base Subset_system_gen.
+Require Import Subset Subset_dec Subset_finite Subset_seq Function.
+Require Import Subset_system_def Subset_system_base Subset_system_gen.
 
 
 Section Subset_systems_Def1.
@@ -2440,7 +2440,7 @@ right; rewrite HA2; apply compl_empty.
 left; rewrite HA2; apply compl_full.
 case (excluded_middle_informative (exists n, A n = fullset)); intros H.
 right; now apply union_seq_full.
-left; apply empty_union_seq; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy.
+left; apply union_seq_empty; intros n; destruct (HA2 n) as [HA2' | HA2']; try easy.
 contradict H; now exists n.
 Qed.
 

Lebesgue/Subset_system_gen.v

@@ -14,7 +14,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-Require Import Subset Subset_system_base.
+Require Import Subset Subset_system_def Subset_system_base.
 
 
 Section Subset_system_Gen_Def0.