Description: Show that double recursion over ordinals yields a function over pairs of ordinals. (Contributed by Scott Fenton, 3-Sep-2024)