Skip to content

Add lemmas `map_intersection_filter` and `map_difference_filter`.

Robbert Krebbers requested to merge robbert/intersection_difference_filter into master

See also the discussion in iris!697 (diffs, comment 69805)

Edited by Robbert Krebbers

Merge request reports