T:Type{i}, U:Type{j}, V:Type{k}, f:(T
UV). f = curry uncurry fT:Type{i}, U:Type{j}, V:Type{k}, f:(T
UV). f = uncurry curry fis mentioned by
| Thm* T:Type{i}, U:Type{j}, V:Type{k}, f:(TUV). f = curry uncurry f | [uncurry_curry_inverse] |
| Thm* T:Type{i}, U:Type{j}, V:Type{k}, f:(TUV). f = uncurry curry f | [curry_uncurry_inverse] |