diff --git a/theories/binders.v b/theories/binders.v
index 1bdd40a0bd27fc2c4ab834e82ea7cf9726da3383..36f9893e9cc5f07a33f7b82865c610826dd51b1e 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -19,6 +19,13 @@ Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
 Global Instance binder_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
 Global Instance binder_inhabited : Inhabited binder := populate BAnon.