Event-B total function proof obligation

Question

I have question as follows: A set A is defined and total function X with invariant type

X ∈ A --> BOOL

and an event A_setSate:

A_setSate =
  WHEN X(A) = TRUE
  THEN X(A) := FALSE

the problem is that the proof obligation event preservation (INV) of A_setState cannot preserve the invariant X∈ A--> BOOL:

I know it is because of the invariant is not strong enough, but I could not create a stronger invariant.

full example : Example snipping

Answer 1

The example looks correct.

Please check if the Atelier B provers are installed, the Rodin Handbook contains instructions for this.

(This answer had been updated after some clarifications in the comments.)