proposition: Lemma del_trans_alt : alternate (bm c0 s0 owner) -> alternate (bm (delete_trans c0 s1) s0 owner).
proof: Proof. case (eq_site_dec s1 s0); intros; simpl in |- *. rewrite e; apply alt_post_dec; trivial. apply alt_post_elsewhere; auto. Qed.
imports: init table_act mess_act