diff --git a/library/leon/collection/List.scala b/library/leon/collection/List.scala
index a7bf09527b530d64e1f29811f7074ef764ae694e..a4db194c3428dd5150025ce575bfa8480a10a015 100644
--- a/library/leon/collection/List.scala
+++ b/library/leon/collection/List.scala
@@ -62,6 +62,8 @@ sealed abstract class List[T] {
     } else {
       tail(index-1)
     }
+  } ensuring {
+    content.contains(_)
   }
 
   @isabelle.function(term = "%xs x. x # xs")