proposition: Lemma rcop2_trans_ctrl_dec : forall s1 : Site, ctrl_dec s0 s1 (bm (rec_copy2_trans c0 s2)) = ctrl_dec s0 s1 (bm c0).
proof: Proof. intros; unfold ctrl_dec in |- *; simpl in |- *. apply diff_collect_card_mess. apply diff_or_elsewhere with (m := copy); [ trivial | discriminate ]. Qed.
imports: init table_act mess_act