proposition: Lemma iter_sepcon_incl_true: forall (p : B -> A) (l s: list B), NoDup s -> incl s l -> iter_sepcon l p |-- iter_sepcon s p * TT.
proof: Proof. intros. destruct (incl_Permutation l s H H0) as [l' ?]. apply (iter_sepcon_permutation p) in H1. rewrite H1, iter_sepcon_app_sepcon. 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