proposition: Lemma binder_delete_delete {A} b s (m : M A) : binder_delete b (delete s m) = delete s (binder_delete b m).
proof: Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
imports: stdpp(sets countable finite fin_maps) stdpp(options)