diff --git a/theories/list.v b/theories/list.v
index 5447d05cc5aea32eea57bd9c3b7cbf9e7e19a65a..f40467c02623fb3df8b8fcfe0e76d017a4956d9d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -581,15 +581,7 @@ Proof.
   * rewrite NoDup_nil.
     setoid_rewrite elem_of_nil. naive_solver.
   * rewrite !NoDup_cons.
-    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
-split.
-destruct IHl.
-intros [??].
-split.
-    naive_solver.
-
-    naive_solver.
-naive_solver.
+    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
 Qed.
 
 Global Instance NoDup_proper: