Skip to content

Strengthen `map_filter_strong_ext` and `map_filter_ext`.

Dan Frumin requested to merge dfrumin/coq-stdpp:map_filter_strong_ext into master

I just added it as another lemma, but it is also possible to change "implies" to "iff" in the map_filter_strong_ext itself.

Edited by Dan Frumin

Merge request reports