proposition: Lemma iter_sepcon_func_derives: forall l P Q, (forall x, In x l -> P x |-- Q x) -> iter_sepcon l P |-- iter_sepcon l Q.
proof: Proof. intros. induction l. - apply derives_refl. - simpl. apply sepcon_derives. + apply H. simpl; auto. + apply IHl. intros; apply H. simpl; 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