diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
index d6a55bbcf..379fba20a 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
@@ -396,12 +396,15 @@ private void constrainIterationElement(
       context.addConstraint(ctx.mkImplies(inBounds, (BoolExpr) selectExpr));
     }
 
-    // Elements of a list, and keys of a map, are CEL values.
-    context.constrainValidValue(
-        ctx.mkAnd(
-            mapPresence == null ? typeSystem.isList(iterRange) : typeSystem.isMap(iterRange),
-            inBounds),
-        xVal);
+    // Elements of a list, and keys of a map, are CEL values. A concrete declared type already
+    // constrains them (performance only).
+    if (!CelZ3OperatorTranslator.hasConcreteElements(context.guaranteedType(iterRange))) {
+      context.constrainValidValue(
+          ctx.mkAnd(
+              mapPresence == null ? typeSystem.isList(iterRange) : typeSystem.isMap(iterRange),
+              inBounds),
+          xVal);
+    }
   }
 
   private TranslatedValue reduceAllOrExists(
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
index 8aaafcd60..d056826e4 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
@@ -659,10 +659,16 @@ private BoolExpr unrollListEquality(
       IntExpr idx = ctx.mkInt(i);
       Expr<?> elem0 = ctx.mkNth(seq0, idx);
       Expr<?> elem1 = ctx.mkNth(seq1, idx);
-      context.constrainValidValue(
-          ctx.mkAnd(typeSystem.isList(listA.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq0))), elem0);
-      context.constrainValidValue(
-          ctx.mkAnd(typeSystem.isList(listB.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq1))), elem1);
+      // A literal's elements, and a concrete declared type's, are already CEL values (performance
+      // only).
+      if (!listA.isLiteral(ExprKind.Kind.LIST) && !hasConcreteElements(type0)) {
+        context.constrainValidValue(
+            ctx.mkAnd(typeSystem.isList(listA.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq0))), elem0);
+      }
+      if (!listB.isLiteral(ExprKind.Kind.LIST) && !hasConcreteElements(type1)) {
+        context.constrainValidValue(
+            ctx.mkAnd(typeSystem.isList(listB.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq1))), elem1);
+      }
 
       if (i >= comprehensionUnrollLimit) {
         constrainListElement(seq0, idx, elem0, type0);
@@ -1138,6 +1144,12 @@ static boolean isStaticallyKnown(CelType type) {
     return !kind.isDyn() && !kind.isTypeParam();
   }
 
+  /** Whether {@code type} is a list or map whose elements (or keys) have a concrete type. */
+  static boolean hasConcreteElements(CelType type) {
+    return (type instanceof ListType || type instanceof MapType)
+        && isConcrete(type.parameters().get(0));
+  }
+
   /** Whether {@code type} and, recursively, its type parameters are statically known. */
   private static boolean isConcrete(CelType type) {
     return isStaticallyKnown(type)