proposition: Lemma select_complete : forall l x, In x l -> f x -> In x (select l).
proof: Proof. induction l; intro x; simpl. fo. intros [h|h]; destruct (f_dec a); subst; fo. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)