proposition: Lemma path_ends_glue: forall g n1 n2 n3 p1 p2, path_ends g p1 n1 n2 -> path_ends g p2 n2 n3 -> path_ends g (p1 +++ p2) n1 n3.
proof: Proof. intros. destruct H, H0. split. icase p1. icase p2. icase p1. simpl in *. subst v0 v. destruct l; simpl. + rewrite app_nil_r. subst. auto. + clear H1. revert H2. induction l0; intros. - rewrite app_nil_l. pose proof (pfoot_head_irrel l g n1 n2 e). unfold pfoot in H. rewrite H. auto. - specialize (IHl0 H2). clear H2. rewrite <- app_comm_cons. simpl. remember (l0 ++ e :: l) as l'. destruct l'; auto. destruct l0; inversion Heql'. 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