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