proposition: Lemma lookup_binder_delete_None {A} (m : M A) b s : binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
proof: Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
imports: stdpp(sets countable finite fin_maps) stdpp(options)