proposition: Lemma compare_eq: forall s s', compare_fun s s' = Eq -> eq s s'.
proof: Proof. unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface