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