a <= k <= b and forall i, a <= i < k : alpha(x,k-1,x[k])[i] = x0[i+1] and forall i, k <= i <= b : alpha(x,k-1,x[k])[i] = x0[i]
a <= k+1 <= b and forall i, a <= i < k+1 : alpha(x,k-1+1,x[k+1])[i] = x0[i+1] and forall i, k+1 <= i <= b : alpha(x,k-1+1,x[k+1])[i] = x0[i]