Description: Restricted "at most one" ( df-wl-rmo ) allows a simplification, if we can assume all occurrences of x in A are bounded. (Contributed by Wolf Lammen, 28-May-2023)