proposition: Lemma corable_andp_wand_corable_andp: forall {A} {NA: NatDed A} {SA: SepLog A} {ClA: ClassicalSep A} {CoA: CorableSepLog A} (P1 P2 Q1 Q2: A), corable P1 -> corable Q1 -> (P1 --> Q1) && (P2 -* Q2) |-- P1 && P2 -* Q1 && Q2.
proof: Proof. intros. rewrite (andp_left_corable P1), (andp_left_corable Q1), (andp_left_corable (P1 --> Q1)) by auto. eapply derives_trans; [| apply wand_sepcon_wand]. apply sepcon_derives; [| auto]. rewrite <- wand_sepcon_adjoint. normalize. rewrite <- andp_assoc. apply andp_derives; [| auto]. rewrite andp_comm; 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