Hi Rustan,
The sequence update is defined so that if 0<=i<ss and
ss' == ss[i:= s]
then
forall i:: 0<=j<ss ==> ss'[j] == if j==i then s else ss[j] .
If that were extended to allow i==ss, implying an append, then we'd have
forall i:: 0<=j<ss' ==> ss'[j] == if j==i then s else ss[j] .
That simplifies coding and reasoning here and there becaue it avoids ifdistinctions (new element or existing?) where conceptually they might not be necessary.
