Doing Alpha Substitutions

P2: INV with x replaced by alpha(x,k-1,x[k])

    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]

P3: P2 with k replaced by k+1

    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]