proposition: Lemma graph_rep_In (g : graph) p: vvalid g p -> graph_rep g = (vertex_at p (vgamma g p) * (vertex_at p (vgamma g p) -* graph_rep g))%logic.
proof: Proof. intros. apply pred_ext. - apply (@vertices_at_ramif_1_stable _ _ _ _ PGBA_VST mpred PGP_VST PGA_VST); auto. - apply modus_ponens_wand. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread CertiGraph.graph.graph_model CertiGraph.msl_application.Graph