proposition: Lemma in_queue_decidable : forall (m : Message) (q : queue Message), {In_queue Message m q} + {~ In_queue Message m q}.
proof: Proof. simple induction q. right; simpl in |- *. simpl in |- *; red in |- *; trivial. intros d q0 H. case (eq_message_dec m d). intro; left; left. trivial. intro; simpl in |- *; elim H. left; right; auto. intro; right; intuition. Qed.
imports: List fifo table reduce sigma2