If the length of the array f is n, and the length of the array invf is m, then this function returns a constraint that ensures that:

• for all i in the interval [0, n-1], if f[i] is in [0, m-1] then invf[f[i]] == i;
• for all j in the interval [0, m-1], if invf[j] is in [0, n-1] then f[invf[j]] == j.