proposition: Lemma graph_rep_In (g : graph) (n: reptype t_struct_tree) p: In (p, n) g -> graph_rep g = (data_at Ews t_struct_tree n p * (data_at Ews t_struct_tree n p -* graph_rep g))%logic.
proof: Proof. intros. apply pred_ext. - induction g; simpl in *. + inversion H. + destruct H as [|]; subst. * simpl. entailer!. apply wand_sepcon_adjoint. entailer!. * specialize (IHg H). sep_apply IHg. entailer. cancel. rewrite <- wand_sepcon_adjoint. cancel. rewrite sepcon_comm. apply modus_ponens_wand. - sep_apply modus_ponens_wand. entailer. Qed.
imports: VST.floyd.proofauto VST.msl.iter_sepcon Demo.treeread