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
feat(frontends/lean): display type of binders, closes #238
feat(quantifiers.lean): change exists_unique to a constructively stronger formulation

the previous formulation was constructively probably to weak to be useful
feat(lean-input.el): add some new notation
feat(library): add definition of subsingleton and some other minor changes
feat(category): split category.lean in different files; add more constructions and theorems about isos
feat(binary.lean): add helper theorem for associative functions
feat(algebra/category/): minor additions, start on adjunction
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
chore(library/algebra/category): add workaround
chore(*): minimize the use of parameters
fix(frontends/lean/elaborator): better specific universe detection