proposition: Lemma copy_trans_diff_site : forall s3 s4 : Site, (In_queue Message copy (bm c0 s3 s4) -> s3 <> s4) -> In_queue Message copy (bm (copy_trans c0 s1 s2) s3 s4) -> s3 <> s4.
proof: Proof. simpl in |- *; intros; case (eq_queue_dec s1 s3 s2 s4); intro. decompose [and] a; rewrite <- H1; rewrite <- H2; trivial. generalize H0; rewrite post_elsewhere; auto. Qed.
imports: init table_act mess_act