proposition: Lemma binder_delete_insert {A} b s x (m : M A) : b ≠ BNamed s → binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
proof: Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
imports: stdpp(sets countable finite fin_maps) stdpp(options)