proposition: Lemma UnIndexedEnsembleListEquivalence_Insert : forall ens (l : list _) a, UnConstrFreshIdx ens (elementIndex a) -> UnIndexedEnsembleListEquivalence ens l -> UnIndexedEnsembleListEquivalence (EnsembleInsert a ens) (indexedElement a :: l).
proof: Proof. unfold UnIndexedEnsembleListEquivalence; intros; intuition. destruct_ex; intuition. subst. eexists (_ :: _); simpl; intuition. - destruct H1; subst; eauto. right; eapply H0; eauto. - econstructor; congruence. - right; eapply H0; eauto. - econstructor. intro. eapply in_map_iff in H1; destruct_ex; intuition; subst. eapply H0 in H4; apply H in H4. omega. 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