proposition: Lemma rdec_trans_diff_site : forall s3 s4 : Site, (In_queue Message copy (bm c0 s3 s4) -> s3 <> s4) -> In_queue Message copy (bm (rec_dec_trans c0 s1 s2) s3 s4) -> s3 <> s4.
proof: Proof. simpl in |- *; intros; apply H. apply in_collect with (s1 := s1) (s2 := s2); trivial. Qed.
imports: init table_act mess_act