proposition: Lemma map_imap_insert {A B} (f : K → A → option B) i x (m : M A) : map_imap f (<[i:=x]> m) = (match f i x with Some y => <[i:=y]> | None => delete i end) (map_imap f m).
proof: Proof. destruct (f i x) as [y|] eqn:Hw; simpl. - apply map_eq. intros k. rewrite map_lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i]. + by rewrite lookup_insert, lookup_insert. + rewrite !lookup_insert_ne by done. by rewrite map_lookup_imap. - apply map_eq. intros k. rewrite map_lookup_imap. destruct (decide (k = i)) as [->|Hk_not_i]. + by rewrite lookup_insert, lookup_delete. + rewrite lookup_insert_ne, lookup_delete_ne by done. by rewrite map_lookup_imap. Qed.
imports: Coq(Permutation) stdpp(options)