fix(library/unifier): handle missing first-order flex-flex case
feat(frontends/lean): elaborate recursive equations

Remark: we are not compiling them yet.