proposition: Lemma nodup_filter: forall A (l: list A) f, NoDup l -> NoDup (filter f l).
proof: Proof. intros. induction l. simpl. constructor. simpl. inversion H. subst. destruct (f a). depremise IHl. assumption. constructor. intro. apply filter_In in H0. destruct H0. contradiction. assumption. apply IHl. assumption. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)