A technical note on universal formula pcas

We record some interesting technical caveats found when using universal formulae to formulate pcas – namely, that there are different ways to extract a (partial) function from a definable collection of pairs, and these choices have an impact on formula complexity.