proposition: Corollary eval_first {x y z : C} (f : x ~> z^y) : eval ∘ first f ≈ uncurry f.
proof: Proof. rewrite <- (curry_uncurry f); cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal Category.Structure.Cartesian Category.Instance.Sets