proposition: Lemma elements_2: forall s x, InL x (elements s) -> In x s.
proof: Proof. unfold elements, In. intros s x H. rewrite xelements_spec in H. destruct H as [H|[y [H H']]]. - inversion_clear H. - rewrite H. assumption. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface