(EE i; 5 <= i <= m+2: H[i] = 2) /\
!(EE i; 5 <= i <= m+2: H[i] < 2)


EE i; 5 <= i <= m+2: H[i] = 2 /\
AA j; 5 <= j <= m+2 /\ j != i: H[j] > 2