doc: improve documentation of `MetavarContext.lean`

[rish987]

This is what I have so far, mainly typo fixes and minor clarifications and a couple new docstrings. I also noticed that the interface of elimMVar could be simplified. I may make a follow-up PR documenting earlier functions in the file, though I am very eager to move on to documenting the frontend code!

[rish987]

Investigating CI...

[Kha]

@rish987 Do you want to revert the elimMVar changes so this can be merged?

[rish987]

Done, thanks for the reminder!

[Kha]

PR was accidentally mislabeled, time to merge!