proposition: Lemma iter_sepcon_permutation: forall (l1 l2 : list B) (p : B -> A), Permutation l1 l2 -> iter_sepcon l1 p = iter_sepcon l2 p.
proof: Proof. intros. induction H; simpl; auto. + rewrite IHPermutation. auto. + do 2 rewrite <- sepcon_assoc. rewrite (sepcon_comm (p y)). auto. + rewrite IHPermutation1. 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