proposition: Lemma path_prop_subpath: forall g P p1 p2, Subpath g p1 p2 -> valid_path g p2 -> path_prop g P p2 -> path_prop g P p1.
proof: Proof. intros. destruct p1 as [v1 p1]. destruct p2 as [v2 p2]. red in H1 |-* . simpl in H1 |-* . destruct H1. destruct H. unfold fst, snd in *. split. 2: eapply Forall_incl; eauto. destruct H3. 1: simpl in H3; subst; easy. destruct H3 as [e [? ?]]. simpl in H3. rewrite Forall_forall in H2. specialize (H2 _ H3). destruct H2. destruct H4; subst; easy. 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