Rm wrong Lift_Trace_is_Subset_rev.

Go for functional equalities.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -376,23 +376,9 @@ induction HB as [P B HB1 HB2].
 apply inter_right in HB2; rewrite <- HB2; easy.
 Qed.
 
-Lemma Lift_Trace_is_Subset_rev :
-  forall (P : set_system U),
-    Union_seq P -> compose (Lift A) (Trace A) P = Subset A P -> P A.
-Proof.
-intros P HP1; rewrite Lift_Trace; setp_any_unfold; intros HP2'.
-assert (HP2 : forall B, image (inter A) P B <-> P B /\ incl B A).
-  intros; rewrite <- Subset_equiv, <- HP2'; easy.
-clear HP2'.
-
-
-
-Admitted.
-
-Lemma Trace_Lift : forall (PA : subset_system A), Trace A (Lift A PA) = PA.
+Lemma Trace_Lift : compose (Trace A) (Lift A) = id.
 Proof.
-intros PA; unfold Trace, tracep_any, Lift, liftp_any.
-rewrite <- image_compose, trace_lift; apply image_id.
+rewrite <- image_id, <- trace_lift, image_compose; easy.
 Qed.
 
 Lemma Trace_monot:
@@ -401,13 +387,13 @@ Proof.
 intros P1 P2 HP BA [B HB]; apply Im; auto.
 Qed.
 
-Lemma Trace_Lift_full : forall (PA : subset_system A), Trace A (Lift_full A PA) = PA.
+Lemma Trace_Lift_full : compose (Trace A) (Lift_full A) = id.
 Proof.
-intros PA; apply Ext_equiv; split; intros BA HBA.
+apply fun_ext; intros PA; apply Ext_equiv; split; intros BA HBA.
 induction HBA as [B HB]; easy.
 apply Trace_monot with (Lift A PA).
 apply Lift_Lift_full.
-rewrite Trace_Lift; easy.
+rewrite <- compose_eq, Trace_Lift; easy.
 Qed.
 
 Lemma Trace_equiv : forall (P : set_system U) B, Trace A P B <-> exists C, P C /\ B = trace A C.
@@ -493,7 +479,7 @@ Lemma Preimage_compose :
 Proof.
 intros P3; unfold Preimage; set_ext_auto A1 HA1; induction HA1 as [A3 HA3].
 rewrite preimage_compose; repeat apply Im; easy.
-induction HA3 as [A3 HA3]; unfold preimagep_any; rewrite preimage_compose_fun.
+induction HA3 as [A3 HA3]; unfold preimagep_any; rewrite preimage_compose.
 apply Im with (f := fun A => preimage f21 (preimage f32 A)); easy.
 Qed.