proposition: Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
proof: Proof. intros; apply NoDup_submseteq; eauto using NoDup_elements. intros x. rewrite !elem_of_elements; auto. Qed.
imports: stdpp(relations) stdpp(options)