proposition: Lemma corable_andp_ocon2 {A} `{CorableOverlapSepLog A}: forall P Q R : A, corable P -> ocon (Q && P) R = P && (ocon Q R).
proof: Proof. intros. rewrite andp_comm. apply corable_andp_ocon1. 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