proposition: Lemma map_imap_delete {A B} (f : K → A → option B) (m : M A) (i : K) : map_imap f (delete i m) = delete i (map_imap f m).
proof: Proof. apply map_eq. intros k. rewrite map_lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i]. - by rewrite !lookup_delete. - rewrite !lookup_delete_ne by done. by rewrite map_lookup_imap. Qed.
imports: Coq(Permutation) stdpp(options)