proposition: Lemma Same_set_ELE {T} (S1 S2 : Ensemble T) (x : list T) (H : Same_set T S1 S2) : EnsembleListEquivalence S1 x <-> EnsembleListEquivalence S2 x.
proof: Proof. intros; split; intros; eapply EnsembleListEquivalence_Same_set; try eassumption. destruct_head_hnf and; split; assumption. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT