proposition: Lemma map_to_set_insert (f : K → A → B)(m : M A) i x : m !! i = None → map_to_set f (<[i:=x]>m) ≡@{C} {[f i x]} ∪ map_to_set f m.
proof: Proof. intros. unfold map_to_set; simpl. by rewrite map_to_list_insert. Qed.
imports: Coq(Permutation) stdpp(options)