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