fact: Definition EnsembleListEquivalence {A} (ensemble : Ensemble A) (seq : list A) := NoDup seq /\ forall x, Ensembles.In _ ensemble x <-> List.In x seq.
imports: Coq.Lists.List Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common Fiat.Common.List.PermutationFacts