How to prevent deletion in an array in the B method
You cannot add such a property to your invariant because the invariant describes how a valid state might look like but not how it can be altered.

The operations are responsible for specifying the behaviour of the model. If you want to prevent that an element will be removed from the array, just do not specify that as a possible behaviour. In your example above, just remove the operation remove.

Every valid refinement is then not allowed to remove an element.