proposition: Remark rcop3_trans_parent : forall s3 s4 : Site, s1 <> s4 \/ s2 <> s3 -> parent (rec_copy3_trans c0 s1 s2) s4 s3 -> parent c0 s4 s3.
proof: Proof. intros; generalize H; elim H0. intros; apply parent_intro. decompose [or] H2. apply rcop3_trans_in_queue with (s1 := s1) (s2 := s2); auto. apply rcop3_trans_in_other_queue with (s1 := s1) (s2 := s2); auto. Qed.
imports: init table_act mess_act