diff --git a/theories/base.v b/theories/base.v
index 682782023a32ba44cefcbed83af7dcc1ba3b49a6..88031b3b4d46c80d1b44e8310b34bc12869fa657 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -937,7 +937,7 @@ Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
   split.
   - induction 1; simpl; auto.
-  - induction l; intros []; subst; constructor; auto.
+  - induction l; destruct 1; subst; constructor; auto.
 Qed.
 
 Inductive NoDup {A} : list A → Prop :=