proposition: Lemma exp_uncurry: forall {A} `{NatDed A} (S T: Type) (P: S -> T -> A), exp (fun s => exp (P s)) = exp (fun st => P (fst st) (snd st)).
proof: Proof. intros. apply pred_ext. + apply exp_left; intro s. apply exp_left; intro t. apply (exp_right (s, t)). apply derives_refl. + apply exp_left; intros [s t]. apply (exp_right s). apply (exp_right t). 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