Inductive invariant validation.

[lemmy]

• https://github.com/apalache-mc/apalache/blob/main/docs/src/apalache/known-issues.md#integer-ranges-with-non-constant-bounds
• https://github.com/apalache-mc/apalache/issues/425
• https://github.com/apalache-mc/apalache/pull/1431

Github issue #5 https://github.com/heidihoward/pbft-tlaplus/issues/5

[Apalache]