proposition: Lemma select_correct : forall l x, In x (select l) -> In x l /\ f x.
proof: Proof. induction l; intro x; simpl. fo. destruct (f_dec a); fo. subst. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)