feat: have `pp.proofs` use `⋯` for omission (#3241)

By having the `pp.proofs` feature use `⋯` when omitting proofs, when
users copy/paste terms from the InfoView the elaborator can give an
error message explaining why the term cannot be elaborated.

Also adds `pp.proofs.threshold` option to allow users to pretty print
shallow proof terms. By default, only atomic proof terms are pretty
printed.

This adjustment was suggested in PR #3201, which added `⋯` and the
related `pp.deepTerms` option.