proposition: Lemma reachable_by_path_app_cons: forall (g: Gph) v p1 e p2 n1 n2 P, g |= (v, p1 ++ e :: p2) is n1 ~o~> n2 satisfying P -> g |= (v, p1) is n1 ~o~> (src g e) satisfying P /\ g |= (dst g e, p2) is (dst g e) ~o~> n2 satisfying P.
proof: Proof. intros. pose proof (reachable_by_path_split_glue g P (v, p1) (src g e, e :: p2) n1 n2 (src g e)). assert (paths_meet_at g (v, p1) (src g e, e :: p2) (src g e)) by (hnf; split; [apply (pfoot_split g v p1 e p2); destruct H as [_ [? _]] | simpl]; auto). specialize (H0 H1 H). destruct H0. split; auto. pose proof (reachable_by_path_split_glue g P (src g e, e :: nil) (dst g e, p2) (src g e) n2 (dst g e)). assert (paths_meet_at g (src g e, e :: nil) (dst g e, p2) (dst g e)) by (hnf; simpl; auto). specialize (H3 H4 H2). destruct H3. 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