proposition: Lemma decide_empty_queue : forall (c : Config) (s1 s2 : Site), {bm c s1 s2 = empty Message} + {bm c s1 s2 <> empty Message}.
proof: Proof. intros. elim (bm c s1 s2). left; auto. simpl in |- *; right. discriminate. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8