proposition: Lemma graph_rep_local_facts g: graph_rep g |-- !!( (forall p v, In (p,v) g -> isptr p) /\ (forall t p, tree_in_graph g t p -> is_pointer_or_null p)).
proof: Proof. rewrite prop_and_mpred. apply andp_right. - rewrite prop_forall; apply allp_right; intros p. rewrite prop_forall; apply allp_right; intros v. rewrite prop_impl. apply imp_andp_adjoint. Intros. rewrite (graph_rep_In _ _ _ H). entailer!. - rewrite prop_forall. apply allp_right. intros t. rewrite prop_forall. apply allp_right. intros v. rewrite prop_impl. apply imp_andp_adjoint. entailer. induction H. + entailer!. + rewrite (graph_rep_In _ _ _ H). entailer!. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread