# Generalize `map_filter_insert` so that it covers both the True and False case.

The new lemma is

```
Lemma map_filter_insert m i x :
filter P (<[i:=x]> m)
= if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
```

We need the `delete`

because there might be another entry with key `i`

in `m`

.

In addition there are the lemmas:

```
Lemma map_filter_insert_True m i x : (* used to be map_filter_insert *)
P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
Lemma map_filter_insert_False m i x : (* used to be map_filter_insert_not_delete *)
¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
```

I use the `_True`

and `_False`

suffixes similar to `decide_True`

and `decide_False`

.

See discussion in !245 (335bc4d6, comment 72118) for the discussion that led to this MR.

Edited by Robbert Krebbers