proposition: Lemma rcop1_trans_in_queue : forall s0 s3 s4 : Site, In_queue Message (inc_dec s0) (bm (rec_copy1_trans c0 s1 s2) s3 s4) -> In_queue Message (inc_dec s0) (bm c0 s3 s4).
proof: Proof. simpl in |- *; intros. apply in_collect with (s1 := s1) (s2 := s2). apply in_post with (m' := dec) (s1 := s2) (s2 := s1). discriminate. auto. Qed.
imports: init table_act mess_act