This changes our uses of sealing to consistently avoid eta-expansion -- except in the proofmode, where I could not figure out what is going on. When I made that sealing conform with our usual patterns, I got conversion errors all over the place (from incorrect unchecked conversion).
Fixes #285 (closed).