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