Clean up `empty{',_inv,_iff}` lemmas.
Write them all using ↔ and consistently use the _iff suffix.
Also:
- Make
map_emptya biimplication - Add lemma
map_filter_empty_iff
Edited by Robbert Krebbers
Write them all using ↔ and consistently use the _iff suffix.
Also:
map_empty a biimplicationmap_filter_empty_iff