proposition: Lemma ppg_out_edges: forall (P: V -> Prop) g1 root g2 (v: V), ~ P root -> (predicate_partialgraph g1 (fun n : V => ~ g1 |= v ~o~> n satisfying P)) ~=~ (predicate_partialgraph g2 (fun n : V => ~ g1 |= v ~o~> n satisfying P)) -> forall e', out_edges g1 root e' <-> out_edges g2 root e'.
proof: Proof. intros. hnf in H0. simpl in H0. unfold predicate_vvalid in H0. unfold predicate_weak_evalid in H0. destruct H0 as [_ [? [? _]]]. specialize (H0 e'). specialize (H1 e'). split; intros; destruct H2; rewrite H3 in * . + assert (evalid g1 e' /\ ~ g1 |= v ~o~> root satisfying P). { split; auto. intro. apply reachable_by_foot_prop in H4. auto. } split; intuition. + assert (evalid g2 e' /\ ~ g1 |= v ~o~> root satisfying P). { split; auto. intro. apply reachable_by_foot_prop in H4. auto. } split; 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