proposition: Lemma iter_sepcon_emp: forall (p : B -> A) (l l' : list B), (forall x, p x |-- emp) -> NoDup l' -> incl l' l -> iter_sepcon l p |-- iter_sepcon l' p.
proof: Proof. intros. revert l H1; induction l'; intros. + simpl; clear H1. induction l; simpl; auto. rewrite <- (emp_sepcon emp). apply sepcon_derives; auto. + inversion H0; subst. spec IHl'; [auto |]. assert (In a l) by (specialize (H1 a); simpl in H1; auto). apply in_split in H2. destruct H2 as [l1 [l2 ?]]. specialize (IHl' (l1 ++ l2)). spec IHl'. 1: { clear - H2 H1 H4. intros x ?H. specialize (H1 x). spec H1; [simpl; auto |]. subst. rewrite in_app_iff in H1; simpl in H1. rewrite in_app_iff. assert (a = x -> False) by (intros; subst; tauto). tauto. } subst. rewrite iter_sepcon_app_sepcon in *. simpl. rewrite (sepcon_comm (p a)), <- sepcon_assoc, (sepcon_comm _ (p a)). apply sepcon_derives; auto. 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