"at" in transformation arguments is silently ignored
In transformation arguments, "at" seems to be silently ignored.
let a = Array.make 10 0
label L in
a[0] <- 0;
assert { true }
If I call cut (a = (a at L)) in the proof of the assertion, the cut indication is "a=a". I have to call "cut (a=a1)" in order to get the desired result.