Generalize `Excl_included` & more `singleton_included` lemmas

• 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