Description: Redefine the restricted existential uniqueness 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-reu |