proposition: Lemma first_copy_diff_site : forall (c0 : Config) (s1 s2 : Site), legal c0 -> first Message (bm c0 s1 s2) = value Message copy -> s1 <> s2.
proof: Proof. intros; apply (copy_diff_site c0 s1 s2). trivial. apply first_in; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc