proposition: Lemma rinc_trans_D : D_queue (bm c0 s0 owner) -> D_queue (bm (rec_inc_trans c0 s1 s2) s0 owner).
proof: Proof. intros; simpl in |- *; apply D_post_elsewhere. auto. apply D_collect; trivial. Qed.
imports: init table_act mess_act