proposition: Lemma map_imap_insert_Some {A B} (f : K → A → option B) i x (m : M A) y : f i x = Some y → map_imap f (<[i:=x]> m) = <[i:=y]> (map_imap f m).
proof: Proof. intros Hi. by rewrite map_imap_insert, Hi. Qed.
imports: Coq(Permutation) stdpp(options)