I think we generally prefer to use already defined constants in the library (at least if the rest of the file is any indication).  Here, I think the forward direction of `equiv_uncurry` from `types.Prod` should be what you want.