proposition: Lemma Same_set__elements_cons__Union {A} x xs : Same_set A (elements (x::xs)) (Union A (Singleton _ x) (elements xs)).
proof: Proof. rewrite !Same_set__elements__Union; simpl; reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List Fiat.ComputationalEnsembles.Core Fiat.Computation Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles