Description: Redefine the restricted "at most one" quantifier context to avoid overloading and syntax check errors in mmj2. This operator is to be distinguished from E* x e. A ph with a similiar semantics, but using x as a formal parameter rather than assuming true elementhood.
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-rmo |