fix(frontends/lean/pp): do not invoke type checker on expressions
containing free variables.

This could happened when the pretty printer was used from Lua to print
nested subterms
fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning.

Thus, the output behavior is the same when we compile lean with/without IGNORE_SORRY=ON
fix(tests/lean/uni_bug1): make sure test does not produce a 'used sorry' warning.