proposition: Lemma sepcon_wand_wand_sepcon: forall {A} `{SepLog A} (P Q R: A), (P -* Q) * R |-- P -* Q * R.
proof: Proof. intros. rewrite <- wand_sepcon_adjoint. rewrite (sepcon_comm _ P), <- sepcon_assoc. apply sepcon_derives; auto. apply modus_ponens_wand. Qed.
imports: VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List CertiGraph.msl_ext.seplog CertiGraph.msl_ext.abs_addr