proposition: Lemma tree_in_graph_null g t: tree_in_graph g t nullval -> graph_rep g |-- !!(t = E).
proof: Proof. intros H. inversion H; subst. - entailer!. - sep_apply (graph_rep_In _ _ _ H0). entailer!. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread