Add Subset_equiv.

Split Lift_Trace_equiv into Lift_Trace_is_Subset{,_rev}.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -341,6 +341,13 @@ Section Subset_Lift_Trace_Facts.
 Context {U : Type}.
 Variable A : set U.
 
+Lemma Subset_equiv :
+  forall (P : set_system U) (B : set U),
+    Subset A P B <-> P B /\ incl B A.
+Proof.
+intros P B; split; intros H; try induction H; easy.
+Qed.
+
 Lemma Lift_Lift_full :
   forall (PA : subset_system A), Incl (Lift A PA) (Lift_full A PA).
 Proof.
@@ -354,25 +361,31 @@ unfold Lift, Trace; setp_any_unfold.
 rewrite <- lift_trace, image_compose; easy.
 Qed.
 
-Lemma Lift_Trace_equiv :
+Lemma Lift_Trace_is_Subset :
   forall (P : set_system U),
-    Inter P ->
-    P A <-> compose (Lift A) (Trace A) P = Subset A P.
+    Inter P -> P A -> compose (Lift A) (Trace A) P = Subset A P.
 Proof.
-intros P HP1; rewrite Lift_Trace; setp_any_unfold; split; intros HP2.
-(* *)
+intros P HP1 HP2; rewrite Lift_Trace; setp_any_unfold.
 apply Ext_equiv; split; intros B HB.
-(* . *)
+(* *)
 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.
+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'.
+
 
-Search inter incl.
 
 Admitted.