feat(kernel/level): add missing normalization rule
test(tests/lean/run): add no_confusion test
fix(frontends/lean): make all variables/parameters visible for 'variables' command
fix(frontends/lean): collect used universe levels after elaboration in the check command
refactor(frontends/lean/notation_cmd): remove unnecessary uses of add_local_expr
feat(util/list_fn): generalize map_filter template
fix(frontends/lean): change how "as-is" expressions are handled

Implicit arguments are consumed.
feat(frontends/lean): add helper function mk_section_local_ref
fix(frontends/lean): bug when using nested sections and parameters

see tests/lean/run/section4.lean