fact: Fixpoint fold_right A B (f:A->B->B) (i:B) (l:list A) := match l with | nil => i | x::L' => f x (fold_right f i L') end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)