proposition: Lemma inc_dec_queue_equal : forall (q : queue Message) (s1 s2 : Site), inc_dec_in_queue s1 q -> inc_dec_in_queue s2 q -> s1 = s2.
proof: Proof. simple induction q. simpl in |- *. intuition. simpl in |- *. intros d q0 s1 s2. intro s0. case d. auto. intro. case (eq_site_dec s s2). case (eq_site_dec s s0). intros. rewrite <- e; rewrite e0. auto. intuition. intuition. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4