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 (proj1 (@CartesianClosedCat.adjoint _ _ _ _ _ CCC _ _ _)). apply (proj1 (@CartesianClosedCat.adjoint _ _ _ _ _ CCC _ _ _)). rewrite CartesianClosedCat.assoc by eauto. rewrite (@CartesianClosedCat.comm _ _ _ _ _ CCC Q P). rewrite <- CartesianClosedCat.assoc by eauto. apply (proj2 (@CartesianClosedCat.adjoint _ _ _ _ _ CCC _ _ _)). apply (proj2 (@CartesianClosedCat.adjoint _ _ _ _ _ CCC _ _ _)). 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