proposition: Lemma ocon_andp_prop': forall {A} `{OverlapSepLog A} P Q R, ocon (!!P && Q) R = !!P && ocon Q R.
proof: Proof. intros. rewrite ocon_comm. rewrite ocon_andp_prop. rewrite ocon_comm. 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