proposition: Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l).
proof: Proof. intros f l; induction l as [|a l IHl]; simpl; auto. intros; inv; auto. destruct (f a); auto. constructor; auto. apply In_InfA; auto. intros y H. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed.
imports: List Sorted Setoid Basics Morphisms