proposition: Lemma Permutation_UnIndexedEnsembleListEquivalence : forall ensemble (l l' : list ElementType), UnIndexedEnsembleListEquivalence ensemble l -> Permutation l l' -> UnIndexedEnsembleListEquivalence ensemble l'.
proof: Proof. simpl; intros. destruct H; intuition; symmetry in H0. destruct (PermutationFacts.permutation_map_base _ H0 _ H1) as [l'' [l''_eq H']]. econstructor; split; intuition eauto. rewrite H'; eapply H; eauto. rewrite H' in H2; eapply H; eauto. eapply PermutationFacts.NoDup_modulo_permutation. eexists (map elementIndex x). intuition. apply Permutation_map. auto. 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