proposition: Lemma Same_set__elements__Union {A} xs : Same_set A (elements xs) (List.fold_right (Union _) (Empty_set _) (map (Singleton _) xs)).
proof: Proof. induction xs; [ | simpl; rewrite <- IHxs; clear IHxs ]; Ensembles_t. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List Fiat.ComputationalEnsembles.Core Fiat.Computation Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles