proposition: Lemma valid_pointer_tree g t p: tree_in_graph g t p -> graph_rep g |-- valid_pointer p.
proof: Proof. intros. inversion H; subst. - entailer !. - rewrite (graph_rep_In g p); auto. simpl vertex_at. auto with valid_pointer. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread CertiGraph.graph.graph_model CertiGraph.msl_application.Graph