Avoid arbitrary terms in `auto using` to make std++ compliant with Coq #12512

This MR provides an alternative to !165 (closed), but avoids the epose horribleness. Instead, it just spells out some proofs, which IMHO makes things easier to maintain.

theories/binders.v

@@ -81,7 +81,7 @@ Section binder_delete_insert.
   Proof. destruct b; solve_proper. Qed.
 
   Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
-  Proof. destruct b; simpl; auto using delete_empty. Qed.
+  Proof. destruct b; simpl; eauto using delete_empty. Qed.
 
   Lemma lookup_binder_delete_None {A} (m : M A) b s :
     binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.