proposition: Lemma epath_to_vpath_pfoot: forall g p l a, epath_to_vpath g p = l +:: a -> pfoot g p = a.
proof: Proof. intros g p. destruct p as [v p]; revert v. induction p; intros. + simpl in *. destruct l. rewrite app_nil_l in H. inversion H; auto. inversion H. destruct l; inversion H2. + simpl in H |-* . destruct p. - destruct l. rewrite app_nil_l in H. inversion H. destruct l. * simpl in H. inversion H. auto. * simpl in H. inversion H. destruct l; inversion H3. - destruct l. 1: rewrite app_nil_l in H; inversion H; destruct p; inversion H2. rewrite <- app_comm_cons in H. pose proof (pfoot_head_irrel p g v (src g e) e). unfold pfoot at 1 in H0. rewrite H0. apply IHp with l. inversion H. simpl. 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