∀ (_x : (_ : ℕ) ×' ℕ),
  ack._unary _x =
    PSigma.casesOn _x fun a a_1 =>
      match a, a_1 with
      | 0, n => n + 1
      | m.succ, 0 => ack._unary ⟨m, 1⟩
      | m.succ, n.succ => ack._unary ⟨m, ack._unary ⟨m + 1, n⟩⟩