proposition: Lemma treerep_local_facts g: graph_rep g |-- !!(forall t p, tree_in_graph g t p -> is_pointer_or_null p).
proof: Proof. do 2 (rewrite prop_forall; apply allp_right; intros). rewrite prop_impl. apply imp_andp_adjoint. entailer. inversion H. - entailer!. - entailer. rewrite (graph_rep_In _ _ H0). simpl vertex_at. entailer!. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread CertiGraph.graph.graph_model CertiGraph.msl_application.Graph