proposition: Lemma enum_trace_uniq (Alpha Beta : nat) : uniq (enum_trace Alpha Beta).
proof: Proof. Proof using. rewrite /enum_trace; apply allpairs_uniq. - exact: trace_seq_uniq. - exact: trace_seq_uniq. - by move=> [i1 i2] [j1 j2]. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure