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