proposition: Lemma pfoot_in_cons: forall g e p v x, pfoot g (v, e :: p) = x -> exists e', In e' (e :: p) /\ dst g e' = x.
proof: Proof. intros. revert v e H. induction p; intros. simpl in H. + exists e. split; auto. apply in_eq. + specialize (IHp (dst g e) a). assert (pfoot g (dst g e, a :: p) = x). { clear IHp. simpl in *. destruct p; auto. pose proof (pfoot_head_irrel p g v (dst g e) e0). unfold pfoot in H0. rewrite H in H0. auto. } specialize (IHp H0). destruct IHp as [e' [? ?]]. exists e'. split; auto. apply in_cons. 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