proposition: Lemma rcop3_trans_diff_site : (In_queue Message copy (bm c0 s3 s4) -> s3 <> s4) -> In_queue Message copy (bm (rec_copy3_trans c0 s1 s2) s3 s4) -> s3 <> s4.
proof: Proof. simpl in |- *; intros; apply H. apply in_collect with (s1 := s1) (s2 := s2). apply in_post with (m' := inc_dec s1) (s1 := s2) (s2 := owner). discriminate. trivial. Qed.
imports: init table_act mess_act