proposition: Lemma exp_ocon1 {A} `{OverlapSepLog A}: forall B (p: B -> A) q, ocon (exp p) q = (exp (fun x => ocon (p x) q)).
proof: Proof. eapply CCC_exp_prod1. apply ocon_owand_CCC. 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