proposition: Lemma rcop3_trans_le_dt_time : dt c0 s0 <= time c0 -> dt (rec_copy3_trans c0 s1 s2) s0 <= time (rec_copy3_trans c0 s1 s2).
proof: Proof. intros; simpl in |- *. case (eq_site_dec s2 s0); intro. rewrite e; rewrite update_here; trivial. rewrite update_elsewhere; auto. Qed.
imports: init table_act mess_act