proposition: Lemma exp_sepcon: forall {A} `{SepLog A} {B} (P Q: B -> A), exp (P * Q) |-- exp P * exp Q.
proof: Proof. intros. apply exp_left; intro. simpl. apply sepcon_derives; apply (exp_right x); apply derives_refl. 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