Highlight inaccessible hypotheses differently in Lean 4

[Julian]

Lean 4 shows inaccessible hypotheses with a trailing cross symbol.

Emacs and VSCode treat these by doing one or both of eliding the cross symbol and highlighting the hypotheses in a dimmer color. We should likely follow suit in some way.

(Follow the resolution in the Zulip thread most likely)