proposition: Lemma extended_copy_vmap_root: forall (g1 g2: Graph) (g1' g2': Graph') x x0 (M: V -> Prop), M x0 -> extended_copy M x (g1, g1') (g2, g2') -> vmap g1 x0 = vmap g2 x0.
proof: Proof. intros. destruct H0 as [_ [? _]]. rewrite guarded_pointwise_relation_spec in H0. apply H0. clear - H; unfold Complement, Ensembles.In; intros ?. apply reachable_by_foot_prop in H0. auto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.lib.List_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.graph_morphism