proposition: Lemma tri_sepcon_ocon {A} `{OverlapSepLog A}: forall P Q R, P * Q * R |-- ocon (P * Q) (Q * R).
proof: Proof. intros. eapply derives_trans; [| apply ocon_wand]. instantiate (1 := Q). rewrite sepcon_assoc. rewrite (sepcon_comm Q R). rewrite <- sepcon_assoc. repeat apply sepcon_derives; auto. + apply wand_sepcon_adjoint; auto. + apply wand_sepcon_adjoint; 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