proposition: Lemma binder_insert_fmap {A B} (f : A → B) (x : A) b (m : M A) : f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
proof: Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
imports: stdpp(sets countable finite fin_maps) stdpp(options)