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