diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml
index 79698ae4..98921582 100644
--- a/specs/java/util/ArrayList.jml
+++ b/specs/java/util/ArrayList.jml
@@ -64,10 +64,17 @@ public class ArrayList<E> extends AbstractList<E>
       @   requires c != null;
       @   requires c.size() <= (Integer.MAX_VALUE/11)*10;
       @   ensures this.size() == c.size();
-      @   ensures (\forall int i; 0 <= i && i < c.size();
-      @                     this.get(i) == (c.iterator().nthNextElement(i)));
       @   ensures capacity == c.size()*1.1;
       @   ensures containsNull == c.containsNull;
+      @   {|
+      @       requires !(c instanceof List);
+      @       ensures (\forall int i; 0 <= i && i < c.size();
+      @                     this.get(i) == (c.iterator().nthNextElement(i)));
+      @       also
+      @       requires c instanceof List;
+      @       ensures (\forall int i; 0 <= i && i < c.size();
+      @                     this.get(i) == ((List) c).get(i));
+      @   |}
       @ also
       @  public exceptional_behavior
       @   requires c == null;