@jdw Good point, I have some text saying I've only really been thinking of the case where the domain of the function has decidable equality, but that is worth emphasizing. The tuples of exponents in my thread have decidable equality, in particular. But thanks for the thoughts of what would happen without that condition.