proposition: Lemma monoid_fold_left_app: forall {f} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) l l', (forall x, f e x === x) -> (forall x, f x e === x) -> (forall x y z, f (f x y) z === f x (f y z)) -> fold_left f (l ++ l') e === f (fold_left f l e) (fold_left f l' e).
proof: Proof. intros. rewrite fold_left_app. generalize (fold_left f l e) as a; clear l; intros. pose proof @monoid_fold_left_head f _ e a l'. simpl in H2. pose proof (proper_fold_left f). rewrite H in H2. auto. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext Coq.Lists.List