More simple changes to make proof mode terms more compact.

This is a follow up of !248 (merged).

Let's wait with merging this MR until the nightly CI is done. Then we can compare the changes w.r.t. having just !248 (merged).