proposition: Lemma empty_queue1 : forall c : Config, legal c -> forall s1 s2 : Site, s1 = s2 -> bm c s1 s2 = empty Message.
proof: Proof. intros. generalize (empty_q_to_me c H s1). rewrite H0. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm