Golf a bijection \$\mathbb{N}^n\to\mathbb{N}\$ Your task is to write a program which implements a bijection \$\mathbb{N}^n\to\mathbb{N}\$ for \$n \ge 1\$. Your program should take \$n\$ natural numbers as input, in any acceptable method (including taking them as a single, \$n\$ element list/array) and output a unique natural number for all possible inputs.
In layman's terms, a bijection \$\mathbb{N}^n\to\mathbb{N}\$ means:

Take \$n\$ natural numbers as input
Map these \$n\$ natural numbers to a single natural number output
For every possible input, the output is provably unique
For every possible output, there exists an input which will give that output

For example, the Cantor pairing function \$\pi : \mathbb{N}^2\to\mathbb{N}\$ is a bijection that takes two natural numbers and maps each pair to a unique natural number.
You may implement whatever bijective function you wish, so long as it is proven to be bijective for all possible inputs. Please include this proof (either directly or through a link) in your answer. This is code-golf so the shortest code, in bytes, wins.
You may decide whether you'd like to use \$\mathbb{N} = \{1, 2, 3, \dots\}\$ or \$\mathbb{N} = \{0, 1, 2, \dots\}\$, so long as this is consistent for all \$n\$.
APL (Dyalog Unicode), 13 10 bytes

(⊢+1⊥∘⍳+)/

Try it online!
Similar to other answers, since the Cantor pairing is bijective, compositing \$n-1\$ Cantor pairings is bijective as well.
(       )/  ⍝ reduce the input with following function
       +    ⍝ left argument + right argument
      ⍳     ⍝ the first left+right positive integers
   1⊥       ⍝ convert those from base 1 (sum)
 ⊢+         ⍝ + right argument