proposition: Lemma map_to_set_insert_L `{!LeibnizEquiv C} (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. unfold_leibniz. apply map_to_set_insert. Qed.
imports: Coq(Permutation) stdpp(options)