Rename `map_filter_lookup` → `map_lookup_filter`.
All the other lemmas are called lookup_OPERATION
or map_lookup_OPERATION
; only the filter one is off. This MR fixes that.
I discovered this while reviewing !459 (merged).
All the other lemmas are called lookup_OPERATION
or map_lookup_OPERATION
; only the filter one is off. This MR fixes that.
I discovered this while reviewing !459 (merged).