proposition: Lemma root_update_ramify1: forall (g: Graph) (x x0: addr) (lx: addr) (gx gx': addr * addr * addr), vvalid g x -> vertices_at (Intersection _ (vvalid (initial_copied_Graph x x0 g)) (fun u : addr => x0 <> u)) (initial_copied_Graph x x0 g) = emp.
proof: Proof. intros. erewrite <- vertices_at_False. apply vertices_at_Same_set. rewrite Same_set_spec; intros ?. Transparent initial_copied_Graph. simpl. Opaque initial_copied_Graph. unfold update_vlabel. if_tac; [| congruence]. split; [intros [? ?]; congruence | tauto]. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas VST.msl.Coqlib2 CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.relation_list CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.graph.graph_morphism CertiGraph.graph.local_graph_copy CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.Graph_Copy Coq.Logic.Classical