Add lemma `binder_delete_empty`.
Passed
Robbert Krebbers
created pipeline for commit
7e0096d8
, finished
For master
10 minutes 33 seconds, queued for 3 seconds