proposition: Lemma parent_dec : forall (c1 : Config) (s1 : Site), {s2 : Site | parent c1 s2 s1} + {(forall s2 : Site, ~ parent c1 s2 s1)}.
proof: Proof. intros; generalize (in_queue_parent_dec c1 s1); intro. elim H; intros y. elim y; intros. left; split with x. apply parent_intro; trivial. right; intro. red in |- *; intro. inversion H0. absurd (In_queue Message (inc_dec s2) (bm c1 s1 owner)); auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc