proposition: Lemma elements_spec1: forall s x, InL x (elements s) <-> In x s.
proof: Proof. unfold elements. intros. rewrite xelements_spec. split; [ intros [A|(y & B & C)] | intros IN ]. - inversion A. - simpl in *. congruence. - right. exists x. auto. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface