feat(bin/linja): add --keep-going N option

Related issue: #234
doc(emacs/README.md): do package-refresh-contents only once

Close #233
doc(emacs/README.md): add 'Unicode' subsection in 'Known Issues' section
fix(emacs/lean-project): use better prompt message for lean-project-create
feat(emacs/lean-settings): enable linja '--keep-going' option

Fix #234
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