Description: Commutation of restricted universal quantifiers. For a version based on fewer axioms see ralcom . (Contributed by Mario Carneiro, 14-Oct-2016)