proposition: Lemma rcop1_trans_alt : alternate (bm c0 s0 owner) -> alternate (bm (rec_copy1_trans c0 s1 s2) s0 owner).
proof: Proof. case (eq_queue_dec s2 s0 s1 owner); intros; simpl in |- *. decompose [and] a; rewrite H0; rewrite H1. apply alt_post_dec. apply alt_collect; trivial. apply alt_post_elsewhere. trivial. apply alt_collect; trivial. Qed.
imports: init table_act mess_act