proposition: Lemma corable_wand_corable: forall {A} {NA: NatDed A} {SA: SepLog A} {ClA: ClassicalSep A} {CoA: CorableSepLog A} (P Q: A), corable P -> corable Q -> P --> Q |-- P -* Q.
proof: Proof. intros. apply wand_sepcon_adjoint. rewrite sepcon_corable_corable, andp_comm; auto. apply modus_ponens. 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