fix(frontends/lean/elaborator): better specific universe detection
feat(library/universe): improve support for universe level constraints in the unifier