proposition: Lemma rinc_trans_alt : alternate (bm c0 s0 owner) -> alternate (bm (rec_inc_trans c0 s1 s2) s0 owner).
proof: Proof. intros; simpl in |- *; apply alt_post_elsewhere. auto. apply alt_collect; trivial. Qed.
imports: init table_act mess_act