Should one provide means to say explicitly that the main existential variable of a given choose rule depends only on such and such of the free variables of the rule? Maybe. But the need for such means has not been demonstrated yet.
