Fixing universe substitution in mutual fixpoints.
Adding a test-suite for bug #3416.