proposition: Theorem eq_message_dec : eq_dec Message.
proof: Proof. unfold eq_dec in |- *; double induction a b; intros. auto. right; discriminate. right; discriminate. right; discriminate. case (eq_site_dec s0 s); intros. rewrite e; auto. right; injection; auto. right; discriminate. right; discriminate. right; discriminate. auto. Qed.
imports: abstract_machine