diff --git a/frontends/library/stainless/collection/List.scala b/frontends/library/stainless/collection/List.scala index 1c9e7cd004..e3bd259c15 100644 --- a/frontends/library/stainless/collection/List.scala +++ b/frontends/library/stainless/collection/List.scala @@ -1300,7 +1300,7 @@ object ListSpecs { val intersection = first & second intersection.forall(first.contains) && intersection.forall(second.contains) && - forall((elem: T) => intersection.contains(elem) == (first.contains(elem) && second.contains(elem))) + intersection.forall(value => first.contains(value) && second.contains(value)) } @opaque