proposition: Lemma path_prop_tail: forall g P p, path_prop g P p -> path_prop g P (ptail g p).
proof: Proof. intros. destruct p as [v p]. red in H |-* . destruct p; simpl in *; auto. destruct H. split. - rewrite Forall_forall in H0. apply (H0 _ (in_eq e p)). - eapply Forall_incl; eauto. apply incl_tl, incl_refl. 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