predicate all_different(array[int] of var int: x) = forall (i,j in 1..length(x) where i