proposition: Lemma exp_allp: forall {A} `{NatDed A} (S T: Type) (P: S -> T -> A), exp (fun s => allp (P s)) |-- allp (fun t => exp (fun s => P s t)).
proof: Proof. intros. apply exp_left; intro s. apply allp_right; intro t. apply (exp_right s). eapply allp_left. 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