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_2, H. - right. abstract (intro H'; rewrite (equal_1 H') in H; discriminate). Defined.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface