proposition: Lemma rcop3_trans_parent_cr : forall s3 s4 : Site, (parent c0 s3 s4 -> dt c0 s3 < dt c0 s4) -> parent (rec_copy3_trans c0 s1 s2) s3 s4 -> dt (rec_copy3_trans c0 s1 s2) s3 < dt (rec_copy3_trans c0 s1 s2) s4.
proof: Proof. simpl in |- *; intros. case (eq_site_dec s2 s3); intro. absurd (parent (rec_copy3_trans c0 s1 s2) s2 s4). apply rcop3_trans_no_parent. auto. red in |- *; intro. elim (no_ancestor_s2 s4); apply short; trivial. rewrite <- e in H0; trivial. rewrite update_elsewhere. case (eq_site_dec s2 s4); intro. rewrite e; rewrite update_here. generalize (le_dt_time s3); omega. rewrite update_elsewhere. apply H; apply rcop3_trans_parent; auto. trivial. trivial. Qed.
imports: init table_act mess_act