proposition: Lemma pfoot_cons: forall g v e p, pfoot g (v, e :: p) = pfoot g (dst g e, p).
proof: Proof. intros. destruct p; simpl; auto. destruct p; auto. apply (pfoot_head_irrel p g v (dst g e) e1). 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