fact: Definition map_ A B1 B2 (F:A->B1->B2) (f:map A B1) : map A B2 := fun (x:A) => match f x with | None => None | Some y => Some (F x y) end.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)