Remove eta-expansions from sealed definitions

As discussed here, we plan to remove all eta-expansions from sealed definitions. That makes the unfolding rewrite more widely applicable.