Description: Restricted universal quantification ( df-wl-ral ) allows allows a simplification, if we can assume all occurrences of x in A are bounded. (Contributed by Wolf Lammen, 26-May-2023)