Use new API (for Lift* and Trace).

Add Trace_monot.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -343,7 +343,8 @@ Variable A : set U.
 
 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 trace_lift; easy.
+intros PA B [BA HBA]; unfold Lift_full;
+    rewrite <- (compose_eq (trace _)), trace_lift; easy.
 Qed.
 
 Lemma Lift_Trace_equiv :
@@ -359,27 +360,23 @@ Admitted.
 
 Lemma Trace_Lift : forall (PA : subset_system A), Trace A (Lift A PA) = PA.
 Proof.
-(*intros PA; unfold Trace, tracep_any, Lift, liftp_any.
-rewrite <- image_compose.
-
-
-
-
-
+intros PA; unfold Trace, tracep_any, Lift, liftp_any.
+rewrite <- image_compose, trace_lift; apply image_id.
+Qed.
 
-; apply Ext_equiv; split; intros BA HBA.
-(* *)
-induction HBA as [B HB]; unfold Lift, liftp_any in HB; rewrite image_eq in HB.
-destruct HB as [BA [HBA1 HBA2]]; rewrite HBA2, trace_lift; easy.
-(* *)
-rewrite <- trace_lift; easy.
-Q*)Admitted.
+Lemma Trace_monot:
+  forall (P1 P2 : set_system U), Incl P1 P2 -> Incl (Trace A P1) (Trace A P2).
+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.
 Proof.
 intros PA; apply Ext_equiv; split; intros BA HBA.
 induction HBA as [B HB]; easy.
-rewrite <- trace_lift; apply Im, Lift_Lift_full; easy.
+apply Trace_monot with (Lift A PA).
+apply Lift_Lift_full.
+rewrite 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.
@@ -396,7 +393,7 @@ Proof.
 intros PA P HPA B HB.
 apply Trace_equiv; exists (lift A B); split.
 apply HPA; easy.
-rewrite trace_lift; easy.
+rewrite <- (compose_eq (trace _)), trace_lift; easy.
 Qed.
 
 End Subset_Lift_Trace_Facts.