Define exponentiation with Gödel's beta function

[lukacslacko]

https://en.wikipedia.org/wiki/G%C3%B6del%27s_%CE%B2_function allows quantification over finite sequences, so if we can implement that, we could define things like exponentiation and factorial using that, and we could prove theorems about them, along the lines of a; b | pow * (a; c | pow) = a; b+c | pow.