fact: Definition filter A B (F:A->B->Prop) (f:map A B) : map A B := fun (x:A) => match f x with | None => None | Some y => If F x y then Some y else None end.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)