proposition: Lemma fmap_insert {A B} (f: A → B) (m : M A) i x : f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
proof: Proof. apply map_eq; intros i'; destruct (decide (i' = i)) as [->|]. - by rewrite lookup_fmap, !lookup_insert. - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done. Qed.
imports: Coq(Permutation) stdpp(options)