proposition: Lemma root_no_in_queue_inc : forall y : Site, ~ In_queue Message (inc_dec y) (bm c0 (root_parent s0) owner).
proof: Proof. intro; red in |- *; intro. elim (root_no_parent y); apply parent_intro; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc