proposition: Remark del_trans_parent : forall s1 s2 : Site, parent (delete_trans c0 s0) s2 s1 -> parent c0 s2 s1.
proof: Proof. intros; elim H. intros; apply parent_intro. apply del_trans_in_queue with (s1 := s0); trivial. Qed.
imports: init table_act mess_act