Mv.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -406,6 +406,14 @@ intros PA B [BA HBA]; unfold Lift_full;
     rewrite <- (compose_eq (trace _)), 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.
+Proof.
+intros B; split.
+intros [C HC]; exists C; easy.
+intros [C [HC HB]]; rewrite HB; easy.
+Qed.
+
 Lemma Lift_Trace : compose (Lift A) (Trace A) = interp_map_any_r A.
 Proof.
 unfold Lift, Trace; setp_any_unfold.
@@ -447,14 +455,6 @@ apply Lift_Lift_full.
 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.
-Proof.
-intros B; split.
-intros [C HC]; exists C; easy.
-intros [C [HC HB]]; rewrite HB; easy.
-Qed.
-
 Lemma Lift_Incl_Incl_Trace :
   forall (PA : subset_system A) (P : set_system U),
     Incl (Lift A PA) P -> Incl PA (Trace A P).