proposition: Lemma pfoot_app_cons: forall g v1 v2 e l1 l2, pfoot g (v1, l1 ++ e :: l2) = pfoot g (v2, e :: l2).
proof: Proof. intros. induction l1. + rewrite app_nil_l. apply pfoot_head_irrel. + rewrite <- app_comm_cons. rewrite <- IHl1. simpl. destruct (l1 ++ e :: l2) eqn:? ; auto. destruct l1; inversion Heql. 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