Nat ->
(\T =>
  [ Var: Nat
  ; Zero: <>
  ; Suc: T
  ; Primrec: <Zero: T; Suc: T; Target: T>
  ; Abs: T
  ; App: <Fun: T; Arg: T>
  ]) ->
(\T =>
  [ Var: Nat
  ; Zero: <>
  ; Suc: T
  ; Primrec: <Zero: T; Suc: T; Target: T>
  ; Abs: T
  ; App: <Fun: T; Arg: T>
  ])