proposition: Lemma del_trans_ctrl_copy : forall s2 : Site, ctrl_copy s0 s2 (bm (delete_trans c0 s1)) = ctrl_copy s0 s2 (bm c0).
proof: Proof. intros; unfold ctrl_copy in |- *; simpl in |- *. apply diff_post_card_mess. left; discriminate. Qed.
imports: init table_act mess_act