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