WIP: add seq results about Trace.

Lebesgue/Set_theory/Set_system/Set_system_base_seq.v

@@ -377,4 +377,16 @@ rewrite <- trace_union_seq; apply Tr, HP, HB.
 apply union_seq_ext; intros n; symmetry; apply HB.
 Qed.
 
+Lemma Trace_Inter_monot_seq : Inter_monot_seq P -> Inter_monot_seq (Trace P V).
+Proof.
+Admitted.
+
+Lemma Trace_Union_monot_seq : Union_monot_seq P -> Union_monot_seq (Trace P V).
+Proof.
+Admitted.
+
+Lemma Trace_Union_disj_seq : Union_disj_seq P -> Union_disj_seq (Trace P V).
+Proof.
+Admitted.
+
 End Seq_Facts3.