From 449fe0dcc41089403b923596152a618f09554c0a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Fri, 17 Jun 2022 14:29:23 +0200
Subject: [PATCH] Use new API (liftp_any). Renaming: Lift' -> Lift_full. Rm
 Trace' (clearly equivalent to the new Trace).

---
 Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
index 0b3780ca..6436346a 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_def_base.v
@@ -118,13 +118,11 @@ Variable A : set U.
 Inductive Subset : set_system U -> set_system U :=
   | Sub : forall (P : set_system U) B, P B -> incl B A -> Subset P B.
 
-Definition Lift : subset_system A -> set_system U := image (lift A).
-Definition Lift' : subset_system A -> set_system U := fun PA B => PA (trace A B).
+Definition Lift : subset_system A -> set_system U := liftp_any A.
+Definition Lift_full : subset_system A -> set_system U := fun PA B => PA (trace A B).
 
 (* Definition 226 p. 40 (v3) *)
-Definition Trace : set_system U -> subset_system A := image (trace A).
-Inductive Trace' : set_system U -> subset_system A :=
-  | Tr : forall (P : set_system U) B, P B -> Trace' P (trace A B).
+Definition Trace : set_system U -> subset_system A := tracep_any A.
 
 End Trace_Def.
 
-- 
GitLab