proposition: Lemma path_prop_equiv: forall g P p, valid_path g p -> (path_prop g P p <-> forall n, In_path g n p -> P n).
proof: Proof. intros. destruct p as [v p]. unfold path_prop. unfold fst, snd. split; intros. - destruct H0. destruct H1. 1: subst; easy. destruct H1 as [e [? ?]]. simpl in H1. rewrite Forall_forall in H2. specialize (H2 _ H1). destruct H2, H3; subst; easy. - split. 1: apply H0; left; auto. rewrite Forall_forall. intros. split; apply H0; right; unfold snd; exists x; split; auto. 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