proposition: Lemma path_glue_assoc: forall (g: Gph) (p1 p2 p3 : path), paths_meet g p1 p2 -> paths_meet g p2 p3 -> (p1 +++ p2) +++ p3 = p1 +++ (p2 +++ p3).
proof: Proof. unfold path_glue. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. destruct p3 as [v3 p3]. simpl. rewrite <- app_assoc. auto. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec