proposition: Lemma pfoot_split: forall g v p1 e p2, valid_path g (v, p1 ++ e :: p2) -> pfoot g (v, p1) = src g e.
proof: Proof. intros g v p1. revert v. induction p1; intros. + simpl. rewrite app_nil_l in H. destruct H. auto. + rewrite <- app_comm_cons in H. specialize (IHp1 (dst g a) e p2). apply valid_path_cons in H. specialize (IHp1 H). simpl. destruct p1. - simpl in IHp1. auto. - rewrite pfoot_head_irrel with (v2 := v) in IHp1. apply IHp1. 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