proposition: Remark rcop3_trans_no_parent : forall s3 s4 : Site, s1 <> s4 \/ s2 <> s3 -> ~ parent c0 s4 s3 -> ~ parent (rec_copy3_trans c0 s1 s2) s4 s3.
proof: Proof. intros; red in |- *; intro; elim H0. apply rcop3_trans_parent; trivial. Qed.
imports: init table_act mess_act