Strengthen `map_filter_strong_ext` and `map_filter_ext`.

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