proposition: Lemma elements_Empty : forall s, Empty s <-> elements s = nil.
proof: Proof. intros. unfold Empty. split; intros. - assert (forall a, ~ List.In a (elements s)). { red; intros. apply (H a). rewrite elements_iff. rewrite InA_alt; exists a; auto. } destruct (elements s); auto. elim (H0 e); simpl; auto. - red; intros. rewrite elements_iff in H0. rewrite InA_alt in H0; destruct H0. rewrite H in H0; destruct H0 as (_,H0); inversion H0. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide