Add Lift_Trace (+ proof).

WIP: Lift_Trace_equiv.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -341,20 +341,38 @@ Section Subset_Lift_Trace_Facts.
 Context {U : Type}.
 Variable A : set U.
 
-Lemma Lift_Lift_full : forall (PA : subset_system A), Incl (Lift A PA) (Lift_full A PA).
+Lemma Lift_Lift_full :
+  forall (PA : subset_system A), Incl (Lift A PA) (Lift_full A PA).
 Proof.
 intros PA B [BA HBA]; unfold Lift_full;
     rewrite <- (compose_eq (trace _)), trace_lift; easy.
 Qed.
 
+Lemma Lift_Trace : compose (Lift A) (Trace A) = interp_map_any_r A.
+Proof.
+unfold Lift, Trace; setp_any_unfold.
+rewrite <- lift_trace, image_compose; easy.
+Qed.
+
 Lemma Lift_Trace_equiv :
-  forall (P : set_system U), P A <-> Lift A (Trace A P) = Subset A P.
+  forall (P : set_system U),
+    Inter P ->
+    P A <-> compose (Lift A) (Trace A) P = Subset A P.
 Proof.
-intros P; split; intros HP.
+intros P HP1; rewrite Lift_Trace; setp_any_unfold; split; intros HP2.
 (* *)
 apply Ext_equiv; split; intros B HB.
-apply Sub.
+(* . *)
+induction HB as [B HB]; apply Sub.
+apply HP1; easy.
+apply inter_lb_l.
+(* . *)
+induction HB as [P B HB1 HB2].
+apply inter_right in HB2; rewrite <- HB2; easy.
+(* *)
+apply Ext_equiv in HP2.
 
+Search inter incl.
 
 Admitted.