feat(frontends/lean): allow 'sorry' implicit argument to access the whole context, and avoid cryptic error message

See new test for explanation.
checkpoint