Use new API (compose/compose3).

Lebesgue/Set_theory/Set_base.v

@@ -121,21 +121,12 @@ Qed.
 
 Lemma lift_trace_lift : compose3 (lift A) (trace A) (lift A) = lift A.
 Proof.
-unfold compose3; rewrite trace_lift.
-
-intros; rewrite trace_lift; easy.
-Qed.
-
-Lemma lift_trace_lift :
-  forall (BA : subset A), lift A (trace A (lift A BA)) = lift A BA.
-Proof.
-intros; rewrite trace_lift; easy.
+unfold compose3; rewrite trace_lift; easy.
 Qed.
 
-Lemma trace_lift_trace :
-  forall (B : set U), trace A (lift A (trace A B)) = trace A B.
+Lemma trace_lift_trace : compose3 (trace A) (lift A) (trace A) = trace A.
 Proof.
-intros; rewrite trace_lift; easy.
+rewrite compose_assoc, trace_lift; easy.
 Qed.
 
 End Prop_Facts0b.
@@ -2076,16 +2067,16 @@ intros Hx3; rewrite (proof_irrelevance _ _ Hx1); auto.
 Qed.
 
 Lemma trace_equiv :
-  forall (A : set U) (BA : subset A) (B : set U),
+  forall (A B : set U) (BA : subset A),
     BA = trace A B <-> inter A B = lift A BA.
 Proof.
-intros A BA B; split; intros HBA.
-rewrite HBA, lift_trace; easy.
+intros A B BA; split; intros H.
+rewrite H, <- lift_trace; easy.
 apply set_ext_equiv; split; intros [x Hx1] Hx2.
-apply (inter_lb_r A _ x); rewrite HBA; apply Lft with Hx1; easy.
+apply (inter_lb_r A _ x); rewrite H; apply Lft with Hx1; easy.
 apply lift_rev.
 replace (fun s => BA s) with BA; try easy. (* FIXME: why? *)
-rewrite <- HBA; easy.
+rewrite <- H; easy.
 Qed.
 
 Lemma trace_empty_equiv :
@@ -2139,12 +2130,12 @@ Qed.
 
 Lemma trace_fullset_l : forall (B : set U), lift fullset (trace fullset B) = B.
 Proof.
-intros; rewrite lift_trace; apply inter_fullset_l.
+intros; rewrite <- (compose_eq (lift _)), lift_trace; apply inter_fullset_l.
 Qed.
 
 Lemma trace_fullset_r_alt : forall (A : set U), lift A (trace A fullset) = A.
 Proof.
-intros; rewrite lift_trace; apply inter_fullset_r.
+intros; rewrite <- (compose_eq (lift _)), lift_trace; apply inter_fullset_r.
 Qed.
 
 Lemma trace_fullset_r : forall (A : set U), trace A fullset = fullset.