Brief typing instructions (opens in a new tab)
The array K is indexed from 0 to M. Please write a predicate saying that the first, second, and last element exist and are different from each other. array_claim K[0...M] M ≥ 2 ∧ K[0] ≠ K[1] ≠ K[M] ≠ K[0] ⇔ M ≥ 2 ∧ K[0] ≠ K[1] ≠ K[M] or