proposition: Lemma trace_seq_uniq l : uniq (trace_seq l).
proof: Proof. Proof using. rewrite map_inj_uniq; first exact: enum_uniq. by move=> i j /rconsK/val_inj ->. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure