proposition: Lemma emp_ocon: forall {A} `{OverlapSepLog A} P, ocon emp P = P.
proof: Proof. intros. rewrite ocon_comm. apply ocon_emp. 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