proposition: Lemma tree_rep_local_facts: forall t p, tree_rep t p |-- !! (is_pointer_or_null p /\ (p=nullval <-> t=E)).
proof: Proof. intros. destruct t; simpl; Intros; try Intros x y; subst; entailer!. + split; auto. + destruct H as [? _]. split; intro. subst. contradiction H. inversion H1. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread