proposition: Lemma fsupp_trace_order A (t : trace A) : fsupp (trace_order t).
proof: Proof. intro y. tertium_non_datur (trace_elems t y). 2: exists nil; ins; eauto with hahn. apply trace_in_nth with (d := y) in H; desc. exists (map (fun i => trace_nth i t y) (List.seq 0 n)). unfold trace_order; ins; desf. ins; in_simp. rewrite trace_nth_indep with (d' := x) in H0; ins. apply trace_nodup_inj in H0; ins; desf. exists i; rewrite trace_nth_indep with (d' := x); splits; ins; in_simp; eauto with hahn. Qed.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription