diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
index 6ad4c8778..14051f148 100644
--- a/backend/cn/lib/check.ml
+++ b/backend/cn/lib/check.ml
@@ -2669,6 +2669,11 @@ let time_check_c_functions (global_var_constraints, (checked : c_function list))
       global.fun_decls
       (return ())
   in
+  let@ () =
+    ListM.iterM
+      (fun (_, (loc, args_and_body)) -> WellTyped.WProc.consistent loc args_and_body)
+      checked
+  in
   let@ errors = check_c_functions checked in
   Cerb_debug.end_csv_timing "type checking functions";
   return errors
diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml
index 981ade6b8..4a0940003 100644
--- a/backend/cn/lib/wellTyped.ml
+++ b/backend/cn/lib/wellTyped.ml
@@ -2319,16 +2319,7 @@ module BaseTyping = struct
 end
 
 module WLabel = struct
-  open Mucore
-
   let typ l = WArgs.typ (fun _body -> False.False) l
-
-  let consistent (loc : Loc.t) (lt : _ expr arguments) : unit m =
-    WArgs.consistent (fun _loc _body -> return ()) "loop/label" loc lt
-
-
-  let welltyped (loc : Loc.t) (lt : _ expr arguments) : _ expr arguments m =
-    WArgs.welltyped (fun _loc body -> return body) "loop/label" loc lt
 end
 
 module WProc = struct
@@ -2363,17 +2354,6 @@ module WProc = struct
     WArgs.consistent
       (fun loc (_body, labels, rt) ->
         let@ () = pure_and_no_initial_resources loc (WRT.consistent loc rt) in
-        let@ () =
-          PmapM.iterM
-            (fun _sym def ->
-              match def with
-              | Return _ -> return ()
-              | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) ->
-                pure_and_no_initial_resources
-                  loc
-                  (WLabel.consistent loc label_args_and_body))
-            labels
-        in
         PmapM.iterM
           (fun _sym def ->
             match def with
@@ -2397,21 +2377,6 @@ module WProc = struct
     WArgs.welltyped
       (fun loc (body, labels, rt) ->
         let@ rt = pure_and_no_initial_resources loc (WRT.welltyped loc rt) in
-        let@ labels =
-          PmapM.mapM
-            (fun _sym def ->
-              match def with
-              | Return loc -> return (Return loc)
-              | Label (loc, label_args_and_body, annots, parsed_spec, loop_info) ->
-                let@ label_args_and_body =
-                  pure_and_no_initial_resources
-                    loc
-                    (WLabel.welltyped loc label_args_and_body)
-                in
-                return (Label (loc, label_args_and_body, annots, parsed_spec, loop_info)))
-            labels
-            Sym.compare
-        in
         let label_context = label_context rt labels in
         let@ labels =
           PmapM.mapM
diff --git a/tests/cn/memcpy.c.verify b/tests/cn/memcpy.c.verify
index 5208f19ec..c354d7b31 100644
--- a/tests/cn/memcpy.c.verify
+++ b/tests/cn/memcpy.c.verify
@@ -17,12 +17,6 @@ tests/cn/memcpy.c:17:16: warning: 'each' expects a 'u64', but 'j' with type 'i32
 tests/cn/memcpy.c:19:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
           take srcInv = each (i32 j; 0i32 <= j && j < n)
                ^
-tests/cn/memcpy.c:17:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
-  /*@ inv take dstInv = each (i32 j; 0i32 <= j && j < n)
-               ^
-tests/cn/memcpy.c:19:16: warning: 'each' expects a 'u64', but 'j' with type 'i32' was provided. This will become an error in the future.
-          take srcInv = each (i32 j; 0i32 <= j && j < n)
-               ^
 tests/cn/memcpy.c:28:30: warning: 'extract' expects a 'u64', but '(i32)read_&i0' with type 'i32' was provided. This will become an error in the future.
     /*@ extract Owned<char>, (i32)i; @*/
                              ^~~~~~