proposition: Lemma relation_list_app: forall {A: Type} (R R': list (relation A)), same_relation _ (relation_list (R ++ R')) (compond_relation (relation_list R) (relation_list R')).
proof: Proof. intros. apply monoid_fold_left_app. + apply compond_eq_left. + apply compond_eq_right. + apply compond_assoc. Qed.
imports: Coq.Classes.Morphisms Coq.Lists.List CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.List_Func_ext CertiGraph.lib.Relation_ext