proposition: Lemma rcop1_trans_parent_cr : forall s3 s4 : Site, (parent c0 s3 s4 -> dt c0 s3 < dt c0 s4) -> parent (rec_copy1_trans c0 s1 s2) s3 s4 -> dt (rec_copy1_trans c0 s1 s2) s3 < dt (rec_copy1_trans c0 s1 s2) s4.
proof: Proof. simpl in |- *; intros; apply H. apply rcop1_trans_parent; trivial. Qed.
imports: init table_act mess_act