refactor(library): move class management to library module
refactor(library): move library/definitional/util module to library
feat(library/definitional/equations): add support for inaccessible patterns
refactor(frontends/lean): move local_context to library
fix(library/unifier): handle missing first-order flex-flex case
feat(frontends/lean): elaborate recursive equations

Remark: we are not compiling them yet.
feat(frontends/lean): elaborate recursive equations