The sequence update is defined so that if 0<=i<|ss| and
ss' == ss[i:= s]
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 if-distinctions (new element or existing?) where conceptually they might not be necessary.