proposition: Lemma iter_sepcon_in_true: forall (p : B -> A) (l : list B) x, In x l -> iter_sepcon l p |-- p x * TT.
proof: Proof. intros. apply in_split in H. destruct H as [l1 [l2 ?]]. subst. rewrite iter_sepcon_app_comm. rewrite <- app_comm_cons. simpl. apply sepcon_derives; auto. apply TT_right. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize