fix(frontends/lean): universe levels associated with section variables should not be fixed in the section
fix(frontends/lean): avoid superfluous local references of the form `@-1 (@ f)`,

This kind of term also confuses the elaborator
fix(frontends/lean): avoid superfluous local references of the form `@-1 (@ f)`,