Brief typing instructions (opens in a new tab)
The array `H` is indexed from `0` and has `l` elements. Write a predicate saying that `H` is a palindrome. array_claim H[0...l-1] f_nodes 20 AA i; 0 <= i < l: H[i] = H[l-i-1] <=> AA i; 0 <= i < l: H[i] = H[l-i] /**/<=> !EE n: n >= 0 /\ n < l /\ H[n] != H[l-1-n] /**/<=> ∀ i; 0 ≤ i < l: H[i] ≤ H[l-1-i] /**/<=> AA i; 0 < i < l: H[i] <= H[l-1-i] or