proposition: Lemma relation_list_tail: forall {A: Type} (l: list (relation A)) a, same_relation _ (relation_list (l ++ a :: nil)) (compond_relation (relation_list l) a).
proof: Proof. intros. apply monoid_fold_left_tail. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.List_Func_ext CertiGraph.lib.Relation_ext