proposition: Remark rinc_trans_parent : forall s3 s4 : Site, parent (rec_inc_trans c0 s1 s2) s4 s3 -> parent c0 s4 s3.
proof: Proof. intros; elim H. intros; apply parent_intro. apply rinc_trans_in_queue with (s1 := s1) (s2 := s2); trivial. Qed.
imports: init table_act mess_act