proposition: Lemma elements_1: forall s x, In x s -> InL x (elements s).
proof: Proof. unfold elements, In. intros. rewrite xelements_spec. right. exists x. auto. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface