proposition: Lemma ppg_the_same_dst: forall (P: V -> Prop) g1 root g2 (v: V) (e : E), ~ P root -> out_edges g1 root e -> (predicate_partialgraph g1 (fun n : V => ~ g1 |= v ~o~> n satisfying P)) ~=~ (predicate_partialgraph g2 (fun n : V => ~ g1 |= v ~o~> n satisfying P)) -> dst g1 e = dst g2 e.
proof: Proof. intros. hnf in H1. simpl in H1. destruct H0. unfold predicate_vvalid in H1. unfold predicate_weak_evalid in H1. destruct H1 as [_ [? [_ ?]]]. specialize (H1 e). specialize (H3 e). rewrite H2 in *. assert (evalid g1 e /\ ~ g1 |= v ~o~> root satisfying P). { split; auto. intro. apply reachable_by_foot_prop in H4. auto. } apply H3; intuition. Qed.
imports: Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind Coq.Logic.Classical