proposition: Lemma paths_meet_cons: forall g v e p1 p2, paths_meet g (v, e :: p1) p2 -> paths_meet g (dst g e, p1) p2.
proof: Proof. intros. destruct H as [? [? ?]]. exists x. split; auto. simpl in H |-* . destruct p1. 1: simpl; auto. pose proof (pfoot_head_irrel p1 g v (dst g e) e0). unfold pfoot in H1. rewrite H in H1. 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