fact: Fixpoint listfilter (L : list A) l := match L with | nil => nil | a :: Q => match l with | nil => nil | true :: q => a :: listfilter Q q | false :: q => listfilter Q q end end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)