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