proposition: Lemma Permutation_EnsembleIndexedListEquivalence : forall ensemble (l l' : list _), EnsembleIndexedListEquivalence ensemble l -> Permutation l l' -> EnsembleIndexedListEquivalence ensemble l'.
proof: Proof. simpl; intros. destruct_EnsembleIndexedListEquivalence. econstructor; eauto. symmetry in H0. destruct (permutation_map_base indexedElement H0 _ eqv_ensemble) as [l'' [l''_eq H']]. econstructor; split; eauto. constructor. - intros; rewrite eqv_nr. split; apply Permutation_in; intuition. - apply NoDup_modulo_permutation. exists (map elementIndex lensemble). 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