proposition: Lemma sepcon_weaken: forall {A} {NA: NatDed A} {SA: SepLog A} (P Q R R': A), R' |-- R -> P |-- Q * R' -> P |-- Q * R.
proof: Proof. intros. eapply derives_trans; eauto. apply sepcon_derives; 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