proposition: Lemma UnIndexedEnsembleListEquivalence_Delete : forall ens (l : list ElementType) P (P_dec : DecideableEnsemble P), UnIndexedEnsembleListEquivalence ens l -> UnIndexedEnsembleListEquivalence (EnsembleDelete ens P) (filter (fun a : ElementType => negb (DecideableEnsembles.dec a)) l).
proof: Proof. unfold UnIndexedEnsembleListEquivalence; intros; intuition. destruct_ex; intuition; subst. eexists; simpl; intuition. symmetry; eapply filter_map. simpl. - destruct H0; subst; eauto. unfold Complement, In in H1. eapply filter_In; split; eauto. eapply H; eauto. rewrite <- Decides_false in H1; rewrite H1; reflexivity. - eapply filter_In in H0; intuition. constructor; eauto. eapply H; eauto. eapply (@Decides_false _ P). destruct (DecideableEnsembles.dec (indexedElement x0)); simpl in *; eauto. - eauto using NoDup_filter_map. 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