diff --git a/lib/Helpers.ml b/lib/Helpers.ml
index e8717904..c615ba2b 100644
--- a/lib/Helpers.ml
+++ b/lib/Helpers.ml
@@ -243,6 +243,8 @@ let is_readonly_builtin_lid lid =
     [ "FStar"; "UInt32" ], "v";
     [ "FStar"; "UInt128" ], "uint128_to_uint64";
     [ "FStar"; "UInt128" ], "uint64_to_uint128";
+    [ "Eurydice" ], "vec_len";
+    [ "Eurydice" ], "vec_index";
   ] in
   List.exists (fun lid' ->
     let lid = Idents.string_of_lident lid in
@@ -292,6 +294,8 @@ class ['self] readonly_visitor = object (self: 'self)
         List.for_all (self#visit_expr_w ()) es
     | EQualified lid when is_readonly_builtin_lid lid ->
         List.for_all (self#visit_expr_w ()) es
+    | ETApp ({ node = EQualified lid; _ }, _) when is_readonly_builtin_lid lid ->
+        List.for_all (self#visit_expr_w ()) es
     | _ ->
         false
 end
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
index 61ef413b..cf9523b6 100644
--- a/lib/Simplify.ml
+++ b/lib/Simplify.ml
@@ -76,6 +76,7 @@ class ['self] safe_use = object (self: 'self)
     match e.node with
     | EOp _ -> super#visit_EApp env e es
     | EQualified lid when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es
+    | ETApp ({ node = EQualified lid; _ }, _) when Helpers.is_readonly_builtin_lid lid -> super#visit_EApp env e es
     | _ -> self#unordered env (e :: es)
 
   method! visit_ELet env _ e1 e2 = self#sequential env e1 (Some e2)