proposition: Lemma monoid_fold_left_tail: forall {f: A -> B -> A} {Proper_f: Proper (equiv ==> equiv ==> equiv) f} (e: A) a l, fold_left f (l ++ a :: nil) e === f (fold_left f l e) a.
proof: Proof. intros. simpl. pose proof (proper_fold_left f). revert e; induction l; intros; simpl. + reflexivity. + apply IHl. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext Coq.Lists.List