The array `H` is indexed from `0` to `m-1`.
Write a predicate saying that a smallest element of `H` is `2`.
array_claim H[0...m-1] f_nodes 30 (EE i; 0 <= i < m: H[i] = 2) /\ !(EE i; 0 <= i < m: H[i] < 2) <=> (EE i; 0 <= i < m: H[i] = 2) /\ !(EE i; 0 <= i < m: H[i] < 2)
Write a predicate saying that the smallest element of `H` is `2`.
array_claim H[0...m-1] f_nodes 30 EE i; 0 <= i < m: H[i] = 2 /\ AA j; 0 <= j < m /\ j != i: H[j] > 2 <=> EE i; 0 <= i < m: H[i] = 2 /\ AA j; 0 <= j < m /\ j != i: H[j] > 2