Skip to content

Clean up `empty{',_inv,_iff}` lemmas.

Robbert Krebbers requested to merge robbert/empty_iff into master

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