proposition: Lemma ppg_reachable_by_path_to: forall (g1 g2 : PreGraph V E) (P Q: V -> Prop) (p: @path V E) (a b: V), (predicate_partialgraph g1 P) ~=~ (predicate_partialgraph g2 P) -> (forall v, In_path g1 v p -> P v) -> g1 |= p is a ~o~> b satisfying Q -> g2 |= p is a ~o~> b satisfying Q.
proof: Proof. intros. assert ((predicate_partialgraph g1 P) |= p is a ~o~> b satisfying Q) by (rewrite <- ppg_reachable_by_path_same; split; auto). rewrite (reachable_by_path_si _ _ _ _ _ _ H) in H2. rewrite <- ppg_reachable_by_path_same in H2. destruct H2; auto. Qed.
imports: Coq.Arith.Arith Coq.Logic.ProofIrrelevance Coq.Logic.FunctionalExtensionality Coq.Classes.Morphisms Coq.Classes.Equivalence CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.relation_list CertiGraph.lib.List_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation