feat(frontends/lean): add option '-X': discard all proofs after theorems are checked

This option is useful for generating compact .olean files for web demos
feat(library/kernel_serializer): compress binder modifier annotations when saving .olean file
refactor(frontends/lean/parser): add missing 'const'
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem
chore(version): bump universe level to force .olean recompilation
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
refactor(library/algebra/category/morphism): make sure bug #231 has been fixed
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
fix(library/module): allow multiple calls to import_modules with the same modules

The idea is to store a set of already imported files.
This feature is useful when using the import_modules API directly (e.g.,
from javascript).
Added closure properties of equivalences.