proposition: Lemma UnIndexedEnsembleListEquivalence_Same_set : forall ens ens' l, Same_set _ ens ens' -> UnIndexedEnsembleListEquivalence ens l -> UnIndexedEnsembleListEquivalence ens' l.
proof: Proof. unfold UnIndexedEnsembleListEquivalence, Same_set, Included; intros; destruct_ex; intuition; subst. eexists _; intuition eauto. eapply H0; eauto. eapply H1; eapply H0; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.String Coq.ZArith.ZArith Coq.Logic.FunctionalExtensionality Coq.Sorting.Permutation Coq.Sets.Ensembles Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts