• Robbert Krebbers's avatar
    Prove Timeless instances in the logic instead of the model. · 0e49878b
    Robbert Krebbers authored
    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).
upred.v 61.5 KB