fact: Fixpoint filter_opt (l : list A) : list B := match l with | nil => nil | cons a m => match f a with | Some b => cons b (filter_opt m) | _ => filter_opt m end end.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)