proposition: Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
proof: Proof. unfold eq. intros. case_eq (equal s s'); intro H. - left. apply equal_spec, H. - right. rewrite <- equal_spec. congruence. Defined.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface