This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.