fix: kill inside a while loop ignored the next iterations (kill)

[strub]

To check that the killed code writes nothing that is read afterwards,
kill collected, with EcMatching.Zipper.after, the code following
the killed code in each enclosing block. For an enclosing while, this
misses the loop guard and the part of the body before the killed code,
which run again on the next iterations. E.g., in

i <- 0; x <- 0; y <- 0;
while (i < 2) { y <- x; x <- x + 1; i <- i + 1; }
return y;

kill 4.2 (x <- x + 1) was accepted, which proves that M.f returns
0 with probability 1 while it returns 1; false follows by byphoare.

kill now uses EcPV.zpr_pv Read After (already used by proc change): the code after the killed code in each enclosing block plus,
for each enclosing loop, its guard and its whole body with the killed
code removed. The rule is sound as the killed code is lossless and the
two programs then run in lockstep on states that agree outside of the
killed writes: everything that runs after (next iterations included)
reads none of them, and neither do the postconditions.

Zipper.after has no other user and is removed.

The issue dates from the introduction of kill (a87e823, 2013-06-04),
so it is present in every tagged release.

tests/kill-loop.ec checks that kill is rejected when the killed
writes are read by the loop guard, by the start of the loop body, or by
an outer loop (killed code in a conditional, spanning the end of a
block, nested loops), and still applies otherwise. The stdlib (128
files), the unit tests (113) and the examples (49) pass.