proposition: Lemma iter_sepcon_map: forall {A B C: Type} {ND : NatDed A} {SL : SepLog A} (l : list C) (f : B -> A) (g: C -> B), iter_sepcon l (fun x : C => f (g x)) = iter_sepcon (map g l) f.
proof: Proof. intros. induction l; simpl; [|f_equal]; 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