proposition: Lemma valid_pointer_tree g t p: tree_in_graph g t p -> graph_rep g |-- valid_pointer p.
proof: Proof. induction 1. - entailer!. - entailer!. eauto using graph_rep_In_valid. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread