Cardinality and Membership

The following operators produce formulas from smaller expression arguments:

• no <expr>: true when <expr> is empty
• lone <expr>: true when <expr> contains zero or one elements
• one <expr>: true when <expr> contains exactly one element
• some <expr>: true when <expr> contains at least one element
• <expr-a> in <expr-b>: true when <expr-a> is a subset of or equal to <expr-b>
• <expr-a> = <expr-b>: true when <expr-a> and <expr-b> contain exactly the same elements