Description: Equivalence of a double universal quantification restricted to the domain and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021)