title: Z3 Checking whether all values in array are unique
body: <p>So I'm trying to check whether all values in an array is unique with the following Z3 code.</p>
  <pre><code>(declare-const A (Array Int Int))
  (declare-const n Int)
  (assert (forall ((i Int) (j Int)) (and (and (and (&gt;= i 0) (&lt; i n)) (and (&gt;= j 0) (&lt; j n)))
                                         (implies (= (select A i) (select A j)) (= i j)))))
  (check-sat)
  </code></pre>
  <p>I'm quite new to Z3 so I don't quite understand the grammar and stuff, but can anyone tell me whether this code is right, and if not, where's the problem?</p>