proposition: Lemma paths_foot_head_meet: forall (g: Gph) p1 p2 n v s, dst g n = v -> paths_meet g (s, p1 +:: n) (v, p2).
proof: Proof. intros. exists v. split. 2: simpl; auto. rewrite pfoot_last. 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