proposition: Lemma is_trace_in_shape (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> in_shape p (a, b).
proof: Proof. Proof using. by move/is_trace_in_in_shape; apply; rewrite inE eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure