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).