proposition: Lemma wand_corable_andp: forall {A} {NA: NatDed A} {SA: SepLog A} {CoA: CorableSepLog A} (P Q R: A), corable Q -> Q && (P -* R) |-- P -* Q && R.
proof: Proof. intros. apply wand_sepcon_adjoint. normalize. apply andp_derives; auto. apply wand_sepcon_adjoint. auto. 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