ghost method z1(ss: seq<int>, l: int, m: int, h: int)
ensures ss[m] in ss[l..h];
does not go through: it gets
input(4,3): Error BP5003: A postcondition might not hold on this return path.
input(3,16): Related location: This is the postcondition that might not hold.
What's the best assertion (or whatever) to stick in there?