proposition: Lemma wand_wand_comm: forall {A} `{SepLog A}, forall P Q R, P -* (Q -* R) = Q -* (P -* R).
proof: Proof. intros. eapply CCC_expo_expo_comm. exact (sepcon_wand_CCC _). 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