proposition: Lemma tree_in_graph_nonnull: forall g t p, p <> nullval -> tree_in_graph g t p -> graph_rep g |-- EX pl pr: val, EX n : int, EX tl tr : tree, graph_rep g && !! (In (p, (Vint n, (pl, pr))) g /\ t = T n tl tr /\ tree_in_graph g tl pl /\ tree_in_graph g tr pr).
proof: Proof. intros. inversion H0; subst. - congruence. - Exists pl pr n tl tr. entailer!. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread