proposition: Lemma rcop1_trans_ctrl_inc : forall s3 : Site, ctrl_inc s0 s3 (bm (rec_copy1_trans c0 s1 s2)) = ctrl_inc s0 s3 (bm c0).
proof: Proof. unfold ctrl_inc in |- *; simpl in |- *; intros. rewrite diff_post_card_mess. rewrite diff_collect_card_mess. auto. apply diff_or_elsewhere with (m := copy); [ trivial | discriminate ]. left; discriminate. Qed.
imports: init table_act mess_act