proposition: Lemma path_prop_si: forall (g1 g2: Gph) P p, g1 ~=~ g2 -> valid_path g1 p -> path_prop g1 P p -> path_prop g2 P p.
proof: Proof. intros. destruct p as [v p]. unfold path_prop in *. simpl in H1 |-* . destruct H1. split; auto. rewrite Forall_forall in *. intros. specialize (H2 _ H3). destruct H as [_ [? [? ?]]]. specialize (H x). specialize (H4 x). specialize (H5 x). destruct (valid_path_strong_evalid _ _ _ _ H0 H3) as [? _]. rewrite <- H4; [|intuition..]. rewrite <- H5; intuition. 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