GitLab

We only had the step-indexed version before. Unfortunately, the non
step-indexed version does not follow from the step-indexed version.

We need to change the core of X from ∅ to X to make elements of gset persistent.

I had to perform some renaming to avoid name clashes.

Annoyingly, this requires one to prove the following in the model:

  (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x)

Thanks to Ranald Clouston for suggesting the axiom:

  ▷ P ⊢ ▷ False ∨ (▷ False → P)

This axiom is used to prove timeless of implication, wand and forall.

Timelessness of the pure and ownM connectives is still proven in the model, but
we first state the property in a way that it does not involved derived notions
(like the except_last modality).

It is unused, and ownM_empty is stronger.

For that we need a slightly stronger property for distributing a later
over an existential quantifier.

Following the time anology of later, the step-index 0 corresponds does
not correspond to 'now', but rather to the end of time (i.e. 'last').