fact: Fixpoint select (l : list A) := match l with | nil => nil | cons a l' => match f_dec a with | left _ => a :: select l' | right _ => select l' end end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)