feat(frontends/lean): add 'universes' command
feat(kernel/inductive): track when K-like reduction can be used