(** * Currying *) (** ** [(yⁿ)ᵐ ≅ yⁿᵐ] *) Require ExponentialLaws.Law4.Functors. Require ExponentialLaws.Law4.Law. Include ExponentialLaws.Law4.Functors. Include ExponentialLaws.Law4.Law.
(** * Currying *) (** ** [(yⁿ)ᵐ ≅ yⁿᵐ] *) Require ExponentialLaws.Law4.Functors. Require ExponentialLaws.Law4.Law. Include ExponentialLaws.Law4.Functors. Include ExponentialLaws.Law4.Law.