proposition: Lemma NoDup_filter_map : forall (f : _ -> bool) (l : list _), NoDup (map elementIndex l) -> NoDup (map elementIndex (filter (fun a => f (indexedElement a)) l)) .
proof: Proof. induction l; simpl. - constructor. - case_eq (f (indexedElement a)); simpl; intros; inversion H0; subst; eauto. constructor; eauto. unfold not; intros; apply H3. revert H1; clear; induction l; simpl. + eauto. + case_eq (f (indexedElement a0)); simpl; intros; intuition. 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