proposition: Lemma CCC_expo_expo_comm: forall A prod expo {ND: NatDed A} {CCC: CCCviaNatDed A prod expo}, forall P Q R, expo P (expo Q R) = expo Q (expo P R).
proof: Proof. intros; apply pred_ext; eapply CCC_expo_expo_comm'; eauto. 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