fact: Definition map A B (f:A->B) (l:list A) : list B := fold_right (fun x acc => (f x)::acc) (@nil B) l.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)