proposition: Lemma sim_concat s0 s1 t0 t1 (EQ0: sim s0 t0) (EQ1: sim s1 t1) : @sim (concat s0 s1) (concat t0 t1) .
proof: Proof. intros. ginit. { eapply cpn2_wcompat; pmonauto. } guclo prefixC_spec. Qed.
imports: Paco.paco Program.Tactics RelationClasses Morphisms