Clean up `empty{',_inv,_iff}` lemmas.
Write them all using ↔
and consistently use the _iff
suffix.
Also:
- Make
map_empty
a biimplication - Add lemma
map_filter_empty_iff
Edited by Robbert Krebbers
Merge request reports
Activity
Please register or sign in to reply