proposition: Lemma tree_rep_valid_pointer: forall t p, tree_rep t p |-- valid_pointer p.
proof: Proof. intros. destruct t; simpl; Intros; try Intros x y; subst; auto with valid_pointer. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread