Some simple lemmas about lists and maps. The lemma map_filter_lookup_eq' generalises map_filter_lookup_eq and can be used to shorten the proof of map_filter_iff.
map_filter_lookup_eq'
map_filter_lookup_eq
map_filter_iff