proposition: Lemma graph_local_facts: forall sh x (g: Graph), weak_valid g x -> @derives mpred Nveric (graph sh x g) (valid_pointer (pointer_val_val x)).
proof: Proof. intros. destruct H. - simpl in H. subst x. entailer!. - eapply derives_trans. + apply (@va_reachable_root_stable_ramify pSGG_VST _ _ _ (sSGG_VST sh) g x (vgamma g x)); auto. + simpl. entailer!. Qed.
imports: CertiGraph.mark.env_mark_bin CertiGraph.graph.graph_model CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph CertiGraph.msl_application.Graph_Mark CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark CertiGraph.floyd_ext.share CertiGraph.mark.spatial_graph_bin_mark