proposition: Lemma diff_or_elsewhere : forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site), first Message (bom s3 s4) = value Message m -> m <> m' -> first Message (bom s1 s2) <> value Message m' \/ s1 <> s3 \/ s2 <> s4.
proof: Proof. intros; case (eq_queue_dec s1 s3 s2 s4); intro. decompose [and] a; rewrite H1; rewrite H2; rewrite H; left; injection; auto. auto. Qed.
imports: List fifo table