proposition: Lemma fold_left_app : forall f i l1 l2, fold_left f i (l1 ++ l2) = fold_left f (fold_left f i l1) l2.
proof: Proof. Proof using. intros. gen i. induction~ l1. { intros. rew_list. do 2 rewrite fold_left_cons. rewrite~ IHl1. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)