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