proposition: Lemma UnIndexedEnsembleListEquivalence_filter : forall R P (P_dec : DecideableEnsemble (A := ElementType) P) l, UnIndexedEnsembleListEquivalence R l -> UnIndexedEnsembleListEquivalence (IndexedEnsemble_Intersection R P) (filter (@DecideableEnsembles.dec _ P P_dec) l).
proof: Proof. destruct 1. eexists (filter (fun x => DecideableEnsembles.dec (indexedElement x)) x); simpl; intuition. - rewrite <- filter_map, H0; reflexivity. - inversion H1. rewrite H in H3. revert H3 H4; clear; induction x; simpl; intuition subst. + apply dec_decides_P in H4; rewrite H4; simpl; intuition. + find_if_inside; simpl; eauto. - apply filter_In in H1; intuition. apply dec_decides_P in H4; econstructor; eauto. apply H; 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