proposition: Lemma pfoot_si: forall (g1 g2: Gph) p, g1 ~=~ g2 -> valid_path g1 p -> pfoot g1 p = pfoot g2 p.
proof: Proof. intros. destruct p as [v p]. revert v H0. induction p; intros. + simpl. auto. + simpl. destruct p. - simpl in H0. destruct H0 as [? [? [? ?]]]. destruct H as [? [? [? ?]]]. specialize (H4 a). apply H6; intuition. - specialize (IHp (dst g1 a)). apply valid_path_cons in H0. specialize (IHp H0). pose proof (pfoot_head_irrel p g1 v (dst g1 a) e). pose proof (pfoot_head_irrel p g2 v (dst g1 a) e). unfold pfoot in *. rewrite H1, H2. apply IHp. 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