bring back some empty_inv lemmas for rewriting

See discussion at !307 (comment 72408)

I think you can remove some items from the sed script now.

Otherwise LGTM

added 1 commit

• 79bf64ed - update sed script

Compare with previous version

resolved all threads

mentioned in commit 10ba5946

merged