Skip to content
GitLab

Generalize `Excl_included` & more `singleton_included` lemmas

Merged Robbert Krebbers requested to merge robbert/some_cmra_lemmas into master
  • Make lemma Excl_included a bi-implication.
  • Add lemma singleton_included : {[ i := x ]} ≼ ({[ i := y ]} ↔ x ≡ y ∨ x ≼ y, and rename existing asymmetric lemmas (with a singleton on just the LHS):
    • singleton_includedN → singleton_includedN_l.
    • singleton_included → singleton_included_l.
    • singleton_included_exclusive → singleton_included_l_exclusive