proposition: Lemma fold_left_cons : forall f i x l, fold_left f i (x::l) = fold_left f (f x i) l.
proof: Proof. Proof using. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)