proposition: Lemma EnsembleListEquivalence_Same_set U (A B : Ensemble U) ls (H : EnsembleListEquivalence A ls) : EnsembleListEquivalence B ls <-> Same_set _ A B.
proof: Proof. induction ls; repeat match goal with | _ => split | _ => intro | _ => progress destruct_head_hnf and | _ => progress split_iff | _ => progress simpl in * | _ => solve [ eauto ] end. Unshelve. assumption. Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common Fiat.Common.List.PermutationFacts