Simplify definition of cancelable invariants.

There is no need to include the `(∃ P', □ ▷ (P  P')  ...` since we
get closure under `▷ □ ` from regular invariants.
6 jobs for master
Status Job ID Name Coverage
  Build
canceled #46417
fp
build-coq.8.10.0

canceled #46416
fp
build-coq.8.10.1

canceled #46420
fp
build-coq.8.8.2

canceled #46419
fp-timing
build-coq.8.9.0

canceled #46418
fp
build-coq.8.9.1

canceled #46415
fp
build-coq.dev