diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
index a80720458..0ffdb0d56 100644
--- a/backend/cn/bin/main.ml
+++ b/backend/cn/bin/main.ml
@@ -322,9 +322,9 @@ let verify
     ~magic_comment_char_dollar (* Callbacks *)
     ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace)
     ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused ->
-      let check (functions, lemmas) =
+      let check (functions, global_var_constraints, lemmas) =
         let open Typing in
-        let@ errors = Check.time_check_c_functions functions in
+        let@ errors = Check.time_check_c_functions (global_var_constraints, functions) in
         if not quiet then
           List.iter
             (fun (fn, err) ->
diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
index e1a561f63..6ad4c8778 100644
--- a/backend/cn/lib/check.ml
+++ b/backend/cn/lib/check.ml
@@ -130,7 +130,7 @@ let rec check_mem_value (loc : Locations.t) ~(expect : BT.t) (mem : mem_value) :
     (fun ity iv ->
       let@ () = WellTyped.WCT.is_ct loc (Integer ity) in
       let bt = Memory.bt_of_sct (Integer ity) in
-      let@ () = WellTyped.ensure_base_type loc ~expect bt in
+      let@ () = ensure_base_type loc ~expect bt in
       return (int_lit_ (Memory.int_of_ival iv) bt loc))
     (fun _ft _fv -> unsupported loc !^"floats")
     (fun ct ptrval ->
@@ -144,7 +144,7 @@ let rec check_mem_value (loc : Locations.t) ~(expect : BT.t) (mem : mem_value) :
       return (make_array_ ~index_bt ~item_bt values loc))
     (fun tag mvals ->
       let@ () = WellTyped.WCT.is_ct loc (Struct tag) in
-      let@ () = WellTyped.ensure_base_type loc ~expect (Struct tag) in
+      let@ () = ensure_base_type loc ~expect (Struct tag) in
       let mvals =
         List.map (fun (id, ct, mv) -> (id, Sctypes.of_ctype_unsafe loc ct, mv)) mvals
       in
@@ -232,18 +232,18 @@ let rec check_value (loc : Locations.t) (Mu.V (expect, v)) : IT.t m =
     let@ () = ensure_base_type loc ~expect (Mu.bt_of_object_value ov) in
     check_object_value loc ov
   | Vctype ct ->
-    let@ () = WellTyped.ensure_base_type loc ~expect CType in
+    let@ () = ensure_base_type loc ~expect CType in
     let ct = Sctypes.of_ctype_unsafe loc ct in
     let@ () = WellTyped.WCT.is_ct loc ct in
     return (IT.const_ctype_ ct loc)
   | Vunit ->
-    let@ () = WellTyped.ensure_base_type loc ~expect Unit in
+    let@ () = ensure_base_type loc ~expect Unit in
     return (IT.unit_ loc)
   | Vtrue ->
-    let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+    let@ () = ensure_base_type loc ~expect Bool in
     return (IT.bool_ true loc)
   | Vfalse ->
-    let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+    let@ () = ensure_base_type loc ~expect Bool in
     return (IT.bool_ false loc)
   | Vfunction_addr sym ->
     let@ () = ensure_base_type loc ~expect (Loc ()) in
@@ -252,7 +252,7 @@ let rec check_value (loc : Locations.t) (Mu.V (expect, v)) : IT.t m =
     return (IT.sym_ (sym, BT.(Loc ()), loc))
   | Vlist (_item_cbt, vals) ->
     let item_bt = Mu.bt_of_value (List.hd vals) in
-    let@ () = WellTyped.ensure_base_type loc ~expect (List item_bt) in
+    let@ () = ensure_base_type loc ~expect (List item_bt) in
     let@ () =
       ListM.iterM (fun i -> ensure_base_type loc ~expect:item_bt (Mu.bt_of_value i)) vals
     in
@@ -511,10 +511,10 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
        let@ binding = get_a sym in
        (match binding with
         | BaseType bt ->
-          let@ () = WellTyped.ensure_base_type loc ~expect bt in
+          let@ () = ensure_base_type loc ~expect bt in
           k (sym_ (sym, bt, loc))
         | Value lvt ->
-          let@ () = WellTyped.ensure_base_type loc ~expect (IT.get_bt lvt) in
+          let@ () = ensure_base_type loc ~expect (IT.get_bt lvt) in
           k lvt)
      | PEval v ->
        let@ () = ensure_base_type loc ~expect (Mu.bt_of_value v) in
@@ -582,7 +582,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
      | Cfvfromint _ -> unsupported loc !^"floats"
      | Civfromfloat _ -> unsupported loc !^"floats"
      | PEarray_shift (pe1, ct, pe2) ->
-       let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in
+       let@ () = ensure_base_type loc ~expect (Loc ()) in
        let@ () = WellTyped.WCT.is_ct loc ct in
        let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe1) in
        let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in
@@ -608,7 +608,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
            in
            k result))
      | PEmember_shift (pe, tag, member) ->
-       let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in
+       let@ () = ensure_base_type loc ~expect (Loc ()) in
        let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
        check_pexpr pe (fun vt ->
          let@ ct = get_struct_member_type loc tag member in
@@ -627,7 +627,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
          in
          k result)
      | PEnot pe ->
-       let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+       let@ () = ensure_base_type loc ~expect Bool in
        let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe) in
        check_pexpr pe (fun vt -> k (not_ vt loc))
      | PEop (op, pe1, pe2) ->
@@ -643,7 +643,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
        in
        (match op with
         | OpDiv ->
-          let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in
+          let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in
           let@ () = WellTyped.ensure_bits_type loc expect in
           let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in
           check_pexpr pe1 (fun v1 ->
@@ -658,7 +658,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
                 let ub = CF.Undefined.UB045a_division_by_zero in
                 fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })))
         | OpRem_t ->
-          let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in
+          let@ () = ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in
           let@ () = WellTyped.ensure_bits_type loc expect in
           let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe2) in
           check_pexpr pe1 (fun v1 ->
@@ -673,63 +673,48 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
                 let ub = CF.Undefined.UB045b_modulo_by_zero in
                 fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })))
         | OpEq ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect Bool in
           let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Mu.bt_of_pexpr pe1)
-              (Mu.bt_of_pexpr pe2)
+            ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2)
           in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (eq_ (v1, v2) loc)))
         | OpGt ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect Bool in
           let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in
           let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Mu.bt_of_pexpr pe1)
-              (Mu.bt_of_pexpr pe2)
+            ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2)
           in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (gt_ (v1, v2) loc)))
         | OpLt ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect Bool in
           let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in
           let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Mu.bt_of_pexpr pe1)
-              (Mu.bt_of_pexpr pe2)
+            ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2)
           in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (lt_ (v1, v2) loc)))
         | OpGe ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect Bool in
           let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in
           let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Mu.bt_of_pexpr pe1)
-              (Mu.bt_of_pexpr pe2)
+            ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2)
           in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (ge_ (v1, v2) loc)))
         | OpLe ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect Bool in
           let@ () = check_cmp_ty (Mu.bt_of_pexpr pe1) in
           let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Mu.bt_of_pexpr pe1)
-              (Mu.bt_of_pexpr pe2)
+            ensure_base_type loc ~expect:(Mu.bt_of_pexpr pe1) (Mu.bt_of_pexpr pe2)
           in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (le_ (v1, v2) loc)))
         | OpAnd ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
-          let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in
-          let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in
+          let@ () = ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in
+          let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (and_ [ v1; v2 ] loc)))
         | OpOr ->
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
-          let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in
-          let@ () = WellTyped.ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in
+          let@ () = ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe1) in
+          let@ () = ensure_base_type loc ~expect:Bool (Mu.bt_of_pexpr pe2) in
           check_pexpr pe1 (fun v1 -> check_pexpr pe2 (fun v2 -> k (or_ [ v1; v2 ] loc)))
         | OpAdd -> not_yet "OpAdd"
         | OpSub ->
@@ -936,7 +921,7 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) (k : IT.t -> unit m) : unit m =
            fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
      | PEis_representable_integer (pe, act) ->
        let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-       let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+       let@ () = ensure_base_type loc ~expect Bool in
        let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe) in
        let ity = Option.get (Sctypes.is_integer_type act.ct) in
        check_pexpr pe (fun arg -> k (is_representable_integer arg ity))
@@ -1338,7 +1323,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
      | Ememop memop ->
        let here = Locations.other __LOC__ in
        let pointer_eq ?(negate = false) pe1 pe2 =
-         let@ () = WellTyped.ensure_base_type loc ~expect Bool in
+         let@ () = ensure_base_type loc ~expect Bool in
          let k, case, res =
            if negate then ((fun x -> k (not_ x loc)), "in", "ptrNeq") else (k, "", "ptrEq")
          in
@@ -1484,9 +1469,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
         | PtrFromInt (act_from, act_to, pe) ->
           let@ () = WellTyped.WCT.is_ct act_from.loc act_from.ct in
           let@ () = WellTyped.WCT.is_ct act_to.loc act_to.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in
+          let@ () = ensure_base_type loc ~expect (Loc ()) in
           let@ () =
-            WellTyped.ensure_base_type
+            ensure_base_type
               loc
               ~expect:(Memory.bt_of_sct act_from.ct)
               (Mu.bt_of_pexpr pe)
@@ -1511,8 +1496,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
         | PtrValidForDeref (act, pe) ->
           (* TODO (DCM, VIP) *)
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
-          let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
+          let@ () = ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
           (* TODO (DCM, VIP): error if called on Void or Function Ctype.
              return false if resource missing *)
           check_pexpr pe (fun arg ->
@@ -1526,8 +1511,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
             k result)
         | PtrWellAligned (act, pe) ->
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect Bool in
-          let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
+          let@ () = ensure_base_type loc ~expect Bool in
+          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
           (* TODO (DCM, VIP): error if called on Void or Function Ctype *)
           check_pexpr pe (fun arg ->
             (* let unspec = CF.Undefined.UB_unspec_pointer_add in *)
@@ -1560,12 +1545,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
             (Loc.other __LOC__)
             !^"PtrMemberShift should be a CHERI only construct"
         | CopyAllocId (pe1, pe2) ->
-          let@ () =
-            WellTyped.ensure_base_type loc ~expect:Memory.uintptr_bt (Mu.bt_of_pexpr pe1)
-          in
-          let@ () =
-            WellTyped.ensure_base_type loc ~expect:BT.(Loc ()) (Mu.bt_of_pexpr pe2)
-          in
+          let@ () = ensure_base_type loc ~expect:Memory.uintptr_bt (Mu.bt_of_pexpr pe1) in
+          let@ () = ensure_base_type loc ~expect:BT.(Loc ()) (Mu.bt_of_pexpr pe2) in
           check_pexpr pe1 (fun vt1 ->
             check_pexpr pe2 (fun vt2 ->
               let unspec = CF.Undefined.UB_unspec_copy_alloc_id in
@@ -1590,7 +1571,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
        (match action_ with
         | Create (pe, act, prefix) ->
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect (Loc ()) in
+          let@ () = ensure_base_type loc ~expect (Loc ()) in
           let@ () = WellTyped.ensure_bits_type loc (Mu.bt_of_pexpr pe) in
           check_pexpr pe (fun arg ->
             let ret_s, ret =
@@ -1641,7 +1622,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
           Cerb_debug.error "todo: Free"
         | Kill (Static ct, pe) ->
           let@ () = WellTyped.WCT.is_ct loc ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect Unit in
+          let@ () = ensure_base_type loc ~expect Unit in
           let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in
           check_pexpr pe (fun arg ->
             let@ _ =
@@ -1657,15 +1638,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
             k (unit_ loc))
         | Store (_is_locking, act, p_pe, v_pe, _mo) ->
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect Unit in
+          let@ () = ensure_base_type loc ~expect Unit in
+          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) in
           let@ () =
-            WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe)
-          in
-          let@ () =
-            WellTyped.ensure_base_type
-              loc
-              ~expect:(Memory.bt_of_sct act.ct)
-              (Mu.bt_of_pexpr v_pe)
+            ensure_base_type loc ~expect:(Memory.bt_of_sct act.ct) (Mu.bt_of_pexpr v_pe)
           in
           check_pexpr p_pe (fun parg ->
             check_pexpr v_pe (fun varg ->
@@ -1704,10 +1680,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
               k (unit_ loc)))
         | Load (act, p_pe, _mo) ->
           let@ () = WellTyped.WCT.is_ct act.loc act.ct in
-          let@ () = WellTyped.ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in
-          let@ () =
-            WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe)
-          in
+          let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in
+          let@ () = ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr p_pe) in
           check_pexpr p_pe (fun pointer ->
             let@ value = load loc pointer act.ct in
             k value)
@@ -1722,7 +1696,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
         | LinuxStore (_ct, _sym1, _sym2, _mo) -> Cerb_debug.error "todo: LinuxStore"
         | LinuxRMW (_ct, _sym1, _sym2, _mo) -> Cerb_debug.error "todo: LinuxRMW")
      | Eskip ->
-       let@ () = WellTyped.ensure_base_type loc ~expect Unit in
+       let@ () = ensure_base_type loc ~expect Unit in
        k (unit_ loc)
      | Eccall (act, f_pe, pes) ->
        let@ () = WellTyped.WCT.is_ct act.loc act.ct in
@@ -1748,7 +1722,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
          in
          (* checks pes against their annotations, and that they match ft's argument types *)
          Spine.calltype_ft loc ~fsym pes ft (fun (Computational ((_, bt), _, _) as rt) ->
-           let@ () = WellTyped.ensure_base_type loc ~expect bt in
+           let@ () = ensure_base_type loc ~expect bt in
            let@ _, members =
              make_return_record
                loc
@@ -1846,7 +1820,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
            in
            eq_ (lhs, rhs) here
        in
-       let@ () = WellTyped.ensure_base_type loc ~expect Unit in
+       let@ () = ensure_base_type loc ~expect Unit in
        let aux loc stmt =
          (* copying bits of code from elsewhere in check.ml *)
          match stmt with
@@ -2077,7 +2051,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
 
 
 let check_expr_top loc labels rt e =
-  let@ () = WellTyped.ensure_base_type loc ~expect:Unit (Mu.bt_of_expr e) in
+  let@ () = ensure_base_type loc ~expect:Unit (Mu.bt_of_expr e) in
   check_expr labels e (fun lvt ->
     let (RT.Computational ((return_s, return_bt), _info, lrt)) = rt in
     match return_bt with
@@ -2280,11 +2254,10 @@ let record_and_check_resource_predicates preds =
     preds
 
 
-let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
+let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> LC.t list m =
   fun globs ->
-  (* TODO: check the expressions *)
-  ListM.iterM
-    (fun (sym, def) ->
+  ListM.fold_leftM
+    (fun acc (sym, def) ->
       match def with
       | Mu.GlobalDef (ct, _) | GlobalDecl ct ->
         let@ () = WellTyped.WCT.is_ct (Loc.other __LOC__) ct in
@@ -2292,12 +2265,10 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
         let info = (Loc.other __LOC__, lazy (Pp.item "global" (Sym.pp sym))) in
         let@ () = add_a sym bt info in
         let here = Locations.other __LOC__ in
-        let@ () =
-          add_c here (LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here))
-        in
+        let good = LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here) in
         let ptr = sym_ (sym, bt, here) in
-        let@ () = add_c here (LC.T (IT.hasAllocId_ ptr here)) in
-        let@ () =
+        let hasAllocId = LC.T (IT.hasAllocId_ ptr here) in
+        let range =
           if !IT.use_vip then
             let module H = Alloc.History in
             let H.{ base; size } = H.(split (lookup_ptr ptr here) here) in
@@ -2311,11 +2282,13 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
                 ]
                 here
             in
-            add_c here (LC.T bounds)
+            [ LC.T bounds ]
           else
-            return ()
+            []
         in
-        return ())
+        (* TODO: check the expressions *)
+        return (good :: hasAllocId :: (range @ acc)))
+    []
     globs
 
 
@@ -2645,8 +2618,7 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   let@ () = record_tagdefs file.tagDefs in
   let@ () = check_tagdefs file.tagDefs in
   let@ () = record_and_check_datatypes file.datatypes in
-  let@ () = init_solver () in
-  let@ () = record_globals file.globs in
+  let@ global_var_constraints = record_globals file.globs in
   let@ () = register_fun_syms file in
   let@ () =
     ListM.iterM (add_stdlib_spec file.call_funinfo) (Sym.Set.elements file.stdlib_syms)
@@ -2662,14 +2634,41 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   let@ _trusted, checked = wf_check_and_record_functions file.funs file.call_funinfo in
   Pp.debug 3 (lazy (Pp.headline "type-checked C functions and specifications."));
   Cerb_debug.end_csv_timing "decl, lemmata, function specification checking";
-  return (List.rev checked, lemmata)
+  return (List.rev checked, global_var_constraints, lemmata)
 
 
 (** With CSV timing enabled, check the provided functions with
     [check_c_functions]. See that function for more information on the
     semantics of checking. *)
-let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t) list m =
+let time_check_c_functions (global_var_constraints, (checked : c_function list))
+  : (string * TypeErrors.t) list m
+  =
   Cerb_debug.begin_csv_timing () (*type checking functions*);
+  let@ () = init_solver () in
+  let here = Locations.other __LOC__ in
+  let@ () = add_cs here global_var_constraints in
+  let@ global = get_global () in
+  let@ () =
+    Sym.Map.fold
+      (fun _ def acc ->
+        (* I think this avoids a left-recursion in the monad bind *)
+        let@ () = WellTyped.WRPD.consistent def in
+        acc)
+      global.resource_predicates
+      (return ())
+  in
+  let@ () =
+    Sym.Map.fold
+      (fun _ (loc, def, _) acc ->
+        match def with
+        | None -> acc
+        | Some def ->
+          (* I think this avoids a left-recursion in the monad bind *)
+          let@ () = WellTyped.WFT.consistent "proc/fun" loc def in
+          acc)
+      global.fun_decls
+      (return ())
+  in
   let@ errors = check_c_functions checked in
   Cerb_debug.end_csv_timing "type checking functions";
   return errors
@@ -2678,7 +2677,17 @@ let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t)
 let generate_lemmas lemmata o_lemma_mode =
   let@ global = get_global () in
   match o_lemma_mode with
-  | Some mode -> lift (Lemmata.generate global mode lemmata)
+  | Some mode ->
+    let@ () =
+      Sym.Map.fold
+        (fun sym (loc, lemma_typ) acc ->
+          (* I think this avoids a left-recursion in the monad bind *)
+          let@ () = WellTyped.WLemma.consistent loc sym lemma_typ in
+          acc)
+        global.lemmata
+        (return ())
+    in
+    lift (Lemmata.generate global mode lemmata)
   | None -> return ()
 
 (* TODO:
diff --git a/backend/cn/lib/resourceInference.ml b/backend/cn/lib/resourceInference.ml
index 07e11f63a..285f1dfb6 100644
--- a/backend/cn/lib/resourceInference.ml
+++ b/backend/cn/lib/resourceInference.ml
@@ -160,7 +160,7 @@ module General = struct
     =
     Pp.(debug 7 (lazy (item __LOC__ (Req.pp (P requested)))));
     let start_timing = Pp.time_log_start __LOC__ "" in
-    let@ oarg_bt = WellTyped.oarg_bt_of_pred loc requested.name in
+    let@ oarg_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in
     let@ provable = provable loc in
     let@ global = get_global () in
     let@ simp_ctxt = simp_ctxt () in
@@ -384,7 +384,7 @@ module General = struct
 
   and qpredicate_request loc uiinfo (requested : Req.QPredicate.t) =
     let@ o_oarg = qpredicate_request_aux loc uiinfo requested in
-    let@ oarg_item_bt = WellTyped.oarg_bt_of_pred loc requested.name in
+    let@ oarg_item_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in
     match o_oarg with
     | None -> return None
     | Some (oarg, rw_time) ->
diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml
index bf1f01786..72d392b29 100644
--- a/backend/cn/lib/typing.ml
+++ b/backend/cn/lib/typing.ml
@@ -72,9 +72,9 @@ let pause_to_result (pause : 'a pause) : 'a Or_TypeError.t = Result.map fst paus
 
 let pure (m : 'a t) : 'a t =
   fun s ->
-  Solver.push (Option.get s.solver);
+  Option.iter Solver.push s.solver;
   let outcome = match m s with Ok (a, _) -> Ok (a, s) | Error e -> Error e in
-  Solver.pop (Option.get s.solver) 1;
+  Option.iter (fun s -> Solver.pop s 1) s.solver;
   outcome
 
 
diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli
index 8d7d646c0..2c0b95fda 100644
--- a/backend/cn/lib/typing.mli
+++ b/backend/cn/lib/typing.mli
@@ -1,5 +1,3 @@
-type solver
-
 type 'a t
 
 type 'a m = 'a t
diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml
index 31312c47f..981ade6b8 100644
--- a/backend/cn/lib/wellTyped.ml
+++ b/backend/cn/lib/wellTyped.ml
@@ -2,29 +2,69 @@ module CF = Cerb_frontend
 module BT = BaseTypes
 module IT = IndexTerms
 module Loc = Locations
-module LC = LogicalConstraints
-module TE = TypeErrors
-module Res = Resource
-module Req = Request
-module Def = Definition
-module LRT = LogicalReturnTypes
-module AT = ArgumentTypes
-module LAT = LogicalArgumentTypes
-module Mu = Mucore
 module IdSet = Set.Make (Id)
-open Context
-open Global
-open TE
-open Pp
-open Typing
+open Pp.Infix
+
+let squotes, warn, dot, string, debug, item, colon, comma =
+  Pp.(squotes, warn, dot, string, debug, item, colon, comma)
+
+
+module type NoSolver = sig
+  (** TODO make this abstract, and one-way lifting functions? *)
+  type 'a m = 'a Typing.t
+
+  (* TODO: different error types for type errors, consistency errors, proof errors *)
+  type failure = Context.t * Explain.log -> TypeErrors.t
+
+  val pure : 'a m -> 'a m
+
+  val fail : failure -> 'a m
+
+  val bound_a : Sym.t -> bool m
+
+  val bound_l : Sym.t -> bool m
+
+  val get_a : Sym.t -> Context.basetype_or_value m
+
+  val get_l : Sym.t -> Context.basetype_or_value m
+
+  val add_a : Sym.t -> BT.t -> Context.l_info -> unit m
+
+  val add_l : Sym.t -> BT.t -> Context.l_info -> unit m
+
+  val get_struct_decl : Loc.t -> Sym.t -> Memory.struct_layout m
+
+  val get_struct_member_type : Loc.t -> Sym.t -> Id.t -> Sctypes.ctype m
+
+  val get_datatype : Loc.t -> Sym.t -> BT.dt_info m
+
+  val get_datatype_constr : Loc.t -> Sym.t -> BT.constr_info m
+
+  val get_resource_predicate_def : Loc.t -> Sym.t -> Definition.Predicate.t m
+
+  val get_logical_function_def : Loc.t -> Sym.t -> Definition.Function.t m
+
+  val get_lemma : Loc.t -> Sym.t -> (Cerb_location.t * ArgumentTypes.lemmat) m
+
+  val get_fun_decl
+    :  Loc.t ->
+    Sym.t ->
+    (Loc.t * ArgumentTypes.ft option * Sctypes.c_concrete_sig) m
+
+  val ensure_base_type : Loc.t -> expect:BT.t -> BT.t -> unit m
+
+  val lift : 'a Or_TypeError.t -> 'a m
+end
+
+open (Typing : NoSolver)
+
+let fail typeErr = fail (fun _ -> typeErr)
 
 open Effectful.Make (Typing)
 
 let use_ity = ref true
 
-let ensure_base_type = Typing.ensure_base_type
-
-let illtyped_index_term (loc : Locations.t) it has ~expected ~reason (_ctxt, _log) =
+let illtyped_index_term (loc : Locations.t) it has ~expected ~reason =
   let reason =
     match reason with
     | Either.Left reason ->
@@ -32,16 +72,14 @@ let illtyped_index_term (loc : Locations.t) it has ~expected ~reason (_ctxt, _lo
       head ^ "\n" ^ pos
     | Either.Right reason -> reason
   in
-  { loc;
-    msg = TypeErrors.Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason }
-  }
+  TypeErrors.
+    { loc; msg = Illtyped_it { it = IT.pp it; has = BT.pp has; expected; reason } }
 
 
 let ensure_bits_type (loc : Loc.t) (has : BT.t) =
   match has with
   | BT.Bits (_sign, _n) -> return ()
-  | has ->
-    fail (fun _ -> { loc; msg = Mismatch { has = BT.pp has; expect = !^"bitvector" } })
+  | has -> fail { loc; msg = Mismatch { has = BT.pp has; expect = !^"bitvector" } }
 
 
 let ensure_z_fits_bits_type loc (sign, n) v =
@@ -49,7 +87,7 @@ let ensure_z_fits_bits_type loc (sign, n) v =
     return ()
   else (
     let err = !^"Value" ^^^ Pp.z v ^^^ !^"does not fit" ^^^ BT.pp (Bits (sign, n)) in
-    fail (fun _ -> { loc; msg = Generic err }))
+    fail { loc; msg = Generic err })
 
 
 let ensure_arith_type ~reason it =
@@ -117,9 +155,9 @@ let ensure_same_argument_number loc input_output has ~expect =
     return ()
   else (
     match input_output with
-    | `General -> fail (fun _ -> { loc; msg = Number_arguments { has; expect } })
-    | `Input -> fail (fun _ -> { loc; msg = Number_input_arguments { has; expect } })
-    | `Output -> fail (fun _ -> { loc; msg = Number_output_arguments { has; expect } }))
+    | `General -> fail { loc; msg = Number_arguments { has; expect } }
+    | `Input -> fail { loc; msg = Number_input_arguments { has; expect } }
+    | `Output -> fail { loc; msg = Number_output_arguments { has; expect } })
 
 
 let compare_by_fst_id (x, _) (y, _) = Id.compare x y
@@ -132,13 +170,13 @@ let correct_members loc (spec : (Id.t * 'a) list) (have : (Id.t * 'b) list) =
         if IdSet.mem id needed then
           return (IdSet.remove id needed)
         else
-          fail (fun _ -> { loc; msg = Unexpected_member (List.map fst spec, id) }))
+          fail { loc; msg = Unexpected_member (List.map fst spec, id) })
       needed
       have
   in
   match IdSet.elements needed with
   | [] -> return ()
-  | missing :: _ -> fail (fun _ -> { loc; msg = Missing_member missing })
+  | missing :: _ -> fail { loc; msg = Missing_member missing }
 
 
 let correct_members_sorted_annotated loc spec have =
@@ -206,8 +244,8 @@ module WBT = struct
     match BT.pick_integer_encoding_type z with
     | Some bt -> return bt
     | None ->
-      fail (fun _ ->
-        { loc; msg = Generic (Pp.item "no standard encoding type for constant" (Pp.z z)) })
+      fail
+        { loc; msg = Generic (Pp.item "no standard encoding type for constant" (Pp.z z)) }
 end
 
 module WCT = struct
@@ -228,6 +266,7 @@ module WCT = struct
 end
 
 module WIT = struct
+  module LC = LogicalConstraints
   open BaseTypes
   open IndexTerms
 
@@ -280,7 +319,7 @@ module WIT = struct
     | [] ->
       assert (List.for_all (function [] -> true | _ -> false) cases);
       (match cases with
-       | [] -> fail (fun _ -> { loc; msg = Generic !^"Incomplete pattern" })
+       | [] -> fail { loc; msg = Generic !^"Incomplete pattern" }
        | _ -> return ())
       (* | [_(\*[]*\)] -> return () *)
       (* | _::_::_ -> fail (fun _ -> {loc; msg = Generic !^"Duplicate pattern"}) *)
@@ -358,7 +397,7 @@ module WIT = struct
               ^/^ !^prev_pos
               ^^ !^suggestion
             in
-            fail (fun _ -> { loc = pat_loc; msg = Redundant_pattern err }))
+            fail { loc = pat_loc; msg = Redundant_pattern err })
         []
         pats
     in
@@ -367,7 +406,7 @@ module WIT = struct
 
   let rec get_location_for_type = function
     | IT (Apply (name, _args), _, loc) ->
-      let@ def = Typing.get_logical_function_def loc name in
+      let@ def = get_logical_function_def loc name in
       return def.loc
     | IT ((MapSet (t, _, _) | Let (_, t)), _, _) -> get_location_for_type t
     | IT (Cons (it, _), _, _) | it -> return @@ IT.get_loc it
@@ -389,7 +428,7 @@ module WIT = struct
           match () with
           | () when is_a -> get_a s
           | () when is_l -> get_l s
-          | () -> fail (fun _ -> { loc; msg = TE.Unknown_variable s })
+          | () -> fail { loc; msg = TypeErrors.Unknown_variable s }
         in
         (match binding with
          | BaseType bt -> return (IT (Sym s, bt, loc))
@@ -718,10 +757,10 @@ module WIT = struct
         let@ () =
           match (IT.get_bt t, cbt) with
           | Integer, Loc () ->
-            fail (fun _ ->
+            fail
               { loc;
                 msg = Generic !^"cast from integer not allowed in bitvector version"
-              })
+              }
           | Loc (), Alloc_id -> return ()
           | Integer, Real -> return ()
           | Real, Integer -> return ()
@@ -741,7 +780,7 @@ module WIT = struct
               ^^^ BT.pp target
               ^^ dot
             in
-            fail (fun _ -> { loc; msg = Generic msg })
+            fail { loc; msg = Generic msg }
         in
         return (IT (Cast (cbt, t), cbt, loc))
       | MemberShift (t, tag, member) ->
@@ -853,14 +892,14 @@ module WIT = struct
           if BT.equal ix_bt (IT.get_bt i) then
             return ()
           else
-            fail (fun _ ->
+            fail
               { loc;
                 msg =
                   Generic
                     (Pp.item
                        "array_to_list: index type disagreement"
                        (Pp.list IT.pp_with_typ [ i; arr ]))
-              })
+              }
         in
         return (IT (ArrayToList (arr, i, len), BT.List bt, loc))
       | MapConst (index_bt, t) ->
@@ -886,7 +925,7 @@ module WIT = struct
            let@ body = infer body in
            return (IT (MapDef ((s, abt), body), Map (abt, IT.get_bt body), loc)))
       | Apply (name, args) ->
-        let@ def = Typing.get_logical_function_def loc name in
+        let@ def = get_logical_function_def loc name in
         let has_args, expect_args = (List.length args, List.length def.args) in
         let@ () = ensure_same_argument_number loc `General has_args ~expect:expect_args in
         let@ args =
@@ -902,7 +941,7 @@ module WIT = struct
         let@ t1 = infer t1 in
         pure
           (let@ () = add_l name (IT.get_bt t1) (loc, lazy (Pp.string "let-var")) in
-           let@ () = add_c loc (LC.T (IT.def_ name t1 loc)) in
+           (* let@ () = add_c loc (LC.T (IT.def_ name t1 loc)) in *)
            let@ t2 = infer t2 in
            return (IT (Let ((name, t1), t2), IT.get_bt t2, loc)))
       | Constructor (s, args) ->
@@ -937,7 +976,7 @@ module WIT = struct
         let@ () = cases_necessary (List.map (fun (pat, _) -> pat) cases) in
         let@ rbt =
           match rbt with
-          | None -> fail (fun _ -> { loc; msg = Empty_pattern })
+          | None -> fail { loc; msg = Empty_pattern }
           | Some rbt -> return rbt
         in
         return (IT (Match (e, cases), rbt, loc))
@@ -965,7 +1004,7 @@ let warn_when_not_quantifier_bt
   (ident : string)
   (loc : Locations.t)
   (bt : BaseTypes.t)
-  (sym : document option)
+  (sym : Pp.document option)
   : unit
   =
   if not (BT.equal bt quantifier_bt) then
@@ -981,6 +1020,7 @@ let warn_when_not_quantifier_bt
 
 
 module WReq = struct
+  module Req = Request
   open IndexTerms
 
   let welltyped loc r =
@@ -989,7 +1029,7 @@ module WReq = struct
       match Req.get_name r with
       | Owned (_ct, _init) -> return []
       | PName name ->
-        let@ def = Typing.get_resource_predicate_def loc name in
+        let@ def = get_resource_predicate_def loc name in
         return def.iargs
     in
     match r with
@@ -1023,16 +1063,16 @@ module WReq = struct
           if Z.lt Z.zero z then
             return step
           else
-            fail (fun _ ->
+            fail
               { loc;
                 msg =
                   Generic (!^"Iteration step" ^^^ IT.pp p.step ^^^ !^"must be positive")
-              })
+              }
         | IT (SizeOf _, _, _) -> return step
         | IT (Cast (_, IT (SizeOf _, _, _)), _, _) -> return step
         | _ ->
           let hint = "Only constant iteration steps are allowed." in
-          fail (fun _ -> { loc; msg = NIA { it = p.step; hint } })
+          fail { loc; msg = NIA { it = p.step; hint } }
       in
       (*let@ () = match p.name with | (Owned (ct, _init)) -> let sz = Memory.size_of_ctype
         ct in if IT.equal step (IT.int_lit_ sz (snd p.q)) then return () else fail (fun _
@@ -1085,23 +1125,22 @@ module WReq = struct
            { name = p.name; pointer; q = p.q; q_loc = p.q_loc; step; permission; iargs })
 end
 
-let oarg_bt_of_pred loc = function
-  | Req.Owned (ct, _init) -> return (Memory.bt_of_sct ct)
-  | Req.PName pn ->
-    let@ def = Typing.get_resource_predicate_def loc pn in
-    return def.oarg_bt
+module WRS = struct
+  let oarg_bt_of_pred loc = function
+    | Request.Owned (ct, _init) -> return (Memory.bt_of_sct ct)
+    | Request.PName pn ->
+      let@ def = get_resource_predicate_def loc pn in
+      return def.oarg_bt
 
 
-let oarg_bt loc = function
-  | Req.P pred -> oarg_bt_of_pred loc pred.name
-  | Req.Q pred ->
-    let@ item_bt = oarg_bt_of_pred loc pred.name in
-    return (BT.make_map_bt (snd pred.q) item_bt)
+  let oarg_bt loc = function
+    | Request.P pred -> oarg_bt_of_pred loc pred.name
+    | Request.Q pred ->
+      let@ item_bt = oarg_bt_of_pred loc pred.name in
+      return (BT.make_map_bt (snd pred.q) item_bt)
 
 
-module WRS = struct
   let welltyped loc (resource, bt) =
-    Pp.(debug 6 (lazy !^__LOC__));
     let@ resource = WReq.welltyped loc resource in
     let@ bt = WBT.is_bt loc bt in
     let@ oarg_bt = oarg_bt loc resource in
@@ -1110,7 +1149,7 @@ module WRS = struct
 end
 
 module WLC = struct
-  type t = LogicalConstraints.t
+  module LC = LogicalConstraints
 
   let welltyped loc lc =
     match lc with
@@ -1127,66 +1166,87 @@ module WLC = struct
 end
 
 module WLRT = struct
+  module LC = LogicalConstraints
   module LRT = LogicalReturnTypes
-  open LRT
 
-  type t = LogicalReturnTypes.t
-
-  let welltyped loc lrt =
+  let consistent loc lrt =
+    let open Typing in
     let rec aux =
       let here = Locations.other __LOC__ in
       function
-      | Define ((s, it), ((loc, _) as info), lrt) ->
+      | LRT.Define ((s, it), ((loc, _) as info), lrt) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
-        let@ it = WIT.infer it in
         let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
         let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in
+        aux lrt
+      | Resource ((s, (re, re_oa_spec)), (loc, _), lrt) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
+        let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in
+        aux lrt
+      | Constraint (lc, info, lrt) ->
+        (* TODO abort early if one of the constraints is the literal fase,
+           so that users are allowed to write such specs *)
+        let@ () = add_c (fst info) lc in
+        aux lrt
+      | I ->
+        let@ provable = provable loc in
+        let here = Locations.other __LOC__ in
+        (match provable (LC.T (IT.bool_ false here)) with
+         | `True ->
+           fail (fun ctxt_log ->
+             { loc; msg = Inconsistent_assumptions ("return type", ctxt_log) })
+         | `False -> return ())
+    in
+    pure (aux lrt)
+
+
+  let welltyped _loc lrt =
+    let rec aux = function
+      | LRT.Define ((s, it), ((loc, _) as info), lrt) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ it = WIT.infer it in
+        let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
         let@ lrt = aux lrt in
-        return (Define ((s, it), info, lrt))
+        return (LRT.Define ((s, it), info, lrt))
       | Resource ((s, (re, re_oa_spec)), ((loc, _) as info), lrt) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
         let@ re, re_oa_spec = WRS.welltyped loc (re, re_oa_spec) in
         let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
-        let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in
         let@ lrt = aux lrt in
-        return (Resource ((s, (re, re_oa_spec)), info, lrt))
+        return (LRT.Resource ((s, (re, re_oa_spec)), info, lrt))
       | Constraint (lc, info, lrt) ->
         let@ lc = WLC.welltyped (fst info) lc in
-        let@ () = add_c (fst info) lc in
         let@ lrt = aux lrt in
-        return (Constraint (lc, info, lrt))
-      | I ->
-        let@ provable = provable loc in
-        let here = Locations.other __LOC__ in
-        let@ () =
-          match provable (LC.T (IT.bool_ false here)) with
-          | `True ->
-            fail (fun ctxt_log ->
-              { loc; msg = Inconsistent_assumptions ("return type", ctxt_log) })
-          | `False -> return ()
-        in
-        return I
+        return (LRT.Constraint (lc, info, lrt))
+      | I -> return LRT.I
     in
     pure (aux lrt)
 end
 
 module WRT = struct
-  type t = ReturnTypes.t
-
   let subst = ReturnTypes.subst
 
   let pp = ReturnTypes.pp
 
+  let consistent loc rt =
+    pure
+      (match rt with
+       | ReturnTypes.Computational ((name, bt), info, lrt) ->
+         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+         let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in
+         WLRT.consistent loc lrt)
+
+
   let welltyped loc rt =
-    Pp.(debug 6 (lazy !^__LOC__));
     pure
       (match rt with
-       | RT.Computational ((name, bt), info, lrt) ->
+       | ReturnTypes.Computational ((name, bt), info, lrt) ->
          (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
          let@ bt = WBT.is_bt (fst info) bt in
          let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in
          let@ lrt = WLRT.welltyped loc lrt in
-         return (RT.Computational ((name, bt), info, lrt)))
+         return (ReturnTypes.Computational ((name, bt), info, lrt)))
 end
 
 (* module WFalse = struct *)
@@ -1200,13 +1260,18 @@ end
 (* end *)
 
 let pure_and_no_initial_resources loc m =
+  let open Typing in
   pure
     (let@ (), _ = map_and_fold_resources loc (fun _re () -> (Deleted, ())) () in
      m)
 
 
 module WLAT = struct
-  let welltyped i_welltyped i_pp kind loc (at : 'i LAT.t) : 'i LAT.t m =
+  module LC = LogicalConstraints
+  module LAT = LogicalArgumentTypes
+
+  let consistent i_welltyped i_pp kind loc (at : 'i LAT.t) : unit m =
+    let open Typing in
     debug
       12
       (lazy
@@ -1216,23 +1281,17 @@ module WLAT = struct
       function
       | LAT.Define ((s, it), info, at) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
-        let@ it = WIT.infer it in
         let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
         let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in
-        let@ at = aux at in
-        return (LAT.Define ((s, it), info, at))
-      | LAT.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) ->
+        aux at
+      | LAT.Resource ((s, (re, re_oa_spec)), (loc, _), at) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
-        let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in
         let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
         let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in
-        let@ at = aux at in
-        return (LAT.Resource ((s, (re, re_oa_spec)), info, at))
+        aux at
       | LAT.Constraint (lc, info, at) ->
-        let@ lc = WLC.welltyped (fst info) lc in
         let@ () = add_c (fst info) lc in
-        let@ at = aux at in
-        return (LAT.Constraint (lc, info, at))
+        aux at
       | LAT.I i ->
         let@ provable = provable loc in
         let here = Locations.other __LOC__ in
@@ -1243,6 +1302,34 @@ module WLAT = struct
               { loc; msg = Inconsistent_assumptions (kind, ctxt_log) })
           | `False -> return ()
         in
+        i_welltyped loc i
+    in
+    pure (aux at)
+
+
+  let welltyped i_welltyped i_pp kind loc (at : 'i LAT.t) : 'i LAT.t m =
+    debug
+      12
+      (lazy
+        (item ("checking wf of " ^ kind ^ " at " ^ Loc.to_string loc) (LAT.pp i_pp at)));
+    let rec aux = function
+      | LAT.Define ((s, it), info, at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ it = WIT.infer it in
+        let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
+        let@ at = aux at in
+        return (LAT.Define ((s, it), info, at))
+      | LAT.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in
+        let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
+        let@ at = aux at in
+        return (LAT.Resource ((s, (re, re_oa_spec)), info, at))
+      | LAT.Constraint (lc, info, at) ->
+        let@ lc = WLC.welltyped (fst info) lc in
+        let@ at = aux at in
+        return (LAT.Constraint (lc, info, at))
+      | LAT.I i ->
         let@ i = i_welltyped loc i in
         return (LAT.I i)
     in
@@ -1250,6 +1337,23 @@ module WLAT = struct
 end
 
 module WAT = struct
+  module AT = ArgumentTypes
+
+  let consistent i_welltyped i_pp kind loc (at : 'i AT.t) : unit m =
+    debug
+      12
+      (lazy
+        (item ("checking wf of " ^ kind ^ " at " ^ Loc.to_string loc) (AT.pp i_pp at)));
+    let rec aux = function
+      | AT.Computational ((name, bt), info, at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in
+        aux at
+      | AT.L at -> WLAT.consistent i_welltyped i_pp kind loc at
+    in
+    pure (aux at)
+
+
   let welltyped i_welltyped i_pp kind loc (at : 'i AT.t) : 'i AT.t m =
     debug
       12
@@ -1270,6 +1374,12 @@ module WAT = struct
 end
 
 module WFT = struct
+  let consistent =
+    WAT.consistent
+      (fun loc rt -> pure_and_no_initial_resources loc (WRT.consistent loc rt))
+      WRT.pp
+
+
   let welltyped =
     WAT.welltyped
       (fun loc rt -> pure_and_no_initial_resources loc (WRT.welltyped loc rt))
@@ -1286,6 +1396,10 @@ end
    (pd.oargs)) *)
 
 module WLArgs = struct
+  module LC = LogicalConstraints
+  module LAT = LogicalArgumentTypes
+  module Mu = Mucore
+
   let rec typ ityp = function
     | Mu.Define (bound, info, lat) -> LAT.Define (bound, info, typ ityp lat)
     | Mu.Resource (bound, info, lat) -> LAT.Resource (bound, info, typ ityp lat)
@@ -1293,32 +1407,26 @@ module WLArgs = struct
     | Mu.I i -> LAT.I (ityp i)
 
 
-  let welltyped (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments_l)
-    : 'j Mu.arguments_l m
+  let consistent (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments_l)
+    : unit m
     =
+    let open Typing in
     let rec aux =
       let here = Locations.other __LOC__ in
-      Pp.(debug 6 (lazy !^__LOC__));
       function
       | Mu.Define ((s, it), ((loc, _) as info), at) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
-        let@ it = WIT.infer it in
         let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
         let@ () = add_c (fst info) (LC.T (IT.def_ s it here)) in
-        let@ at = aux at in
-        return (Mu.Define ((s, it), info, at))
-      | Mu.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) ->
+        aux at
+      | Mu.Resource ((s, (re, re_oa_spec)), (loc, _), at) ->
         (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
-        let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in
         let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
         let@ () = add_r loc (re, O (IT.sym_ (s, re_oa_spec, here))) in
-        let@ at = aux at in
-        return (Mu.Resource ((s, (re, re_oa_spec)), info, at))
+        aux at
       | Mu.Constraint (lc, info, at) ->
-        let@ lc = WLC.welltyped (fst info) lc in
         let@ () = add_c (fst info) lc in
-        let@ at = aux at in
-        return (Mu.Constraint (lc, info, at))
+        aux at
       | Mu.I i ->
         let@ provable = provable loc in
         let here = Locations.other __LOC__ in
@@ -1329,6 +1437,32 @@ module WLArgs = struct
               { loc; msg = Inconsistent_assumptions (kind, ctxt_log) })
           | `False -> return ()
         in
+        i_welltyped loc i
+    in
+    pure (aux at)
+
+
+  let welltyped (i_welltyped : Loc.t -> 'i -> 'j m) _kind loc (at : 'i Mu.arguments_l)
+    : 'j Mu.arguments_l m
+    =
+    let rec aux = function
+      | Mu.Define ((s, it), ((loc, _) as info), at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ it = WIT.infer it in
+        let@ () = add_l s (IT.get_bt it) (loc, lazy (Pp.string "let-var")) in
+        let@ at = aux at in
+        return (Mu.Define ((s, it), info, at))
+      | Mu.Resource ((s, (re, re_oa_spec)), ((loc, _) as info), at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ re, re_oa_spec = WRS.welltyped (fst info) (re, re_oa_spec) in
+        let@ () = add_l s re_oa_spec (loc, lazy (Pp.string "let-var")) in
+        let@ at = aux at in
+        return (Mu.Resource ((s, (re, re_oa_spec)), info, at))
+      | Mu.Constraint (lc, info, at) ->
+        let@ lc = WLC.welltyped (fst info) lc in
+        let@ at = aux at in
+        return (Mu.Constraint (lc, info, at))
+      | Mu.I i ->
         let@ i = i_welltyped loc i in
         return (Mu.I i)
     in
@@ -1336,11 +1470,34 @@ module WLArgs = struct
 end
 
 module WArgs = struct
+  module AT = ArgumentTypes
+  module Mu = Mucore
+
   let rec typ ityp = function
     | Mu.Computational (bound, info, at) -> AT.Computational (bound, info, typ ityp at)
     | Mu.L lat -> AT.L (WLArgs.typ ityp lat)
 
 
+  let consistent : (Loc.t -> 'i -> 'j m) -> string -> Loc.t -> 'i Mu.arguments -> unit m =
+    fun (i_welltyped : Loc.t -> 'i -> 'j m) kind loc (at : 'i Mu.arguments) ->
+    debug 6 (lazy !^__LOC__);
+    debug
+      12
+      (lazy
+        (item
+           ("checking consistency of " ^ kind ^ " at " ^ Loc.to_string loc)
+           (CF.Pp_ast.pp_doc_tree
+              (Mucore.dtree_of_arguments (fun _i -> Dleaf !^"...") at))));
+    let rec aux = function
+      | Mu.Computational ((name, bt), info, at) ->
+        (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+        let@ () = add_a name bt (fst info, lazy (Sym.pp name)) in
+        aux at
+      | Mu.L at -> WLArgs.consistent i_welltyped kind loc at
+    in
+    pure (aux at)
+
+
   let welltyped
     : 'i 'j.
     (Loc.t -> 'i -> 'j m) -> string -> Loc.t -> 'i Mu.arguments -> 'j Mu.arguments m
@@ -1369,7 +1526,6 @@ module WArgs = struct
 end
 
 module BaseTyping = struct
-  open Typing
   open TypeErrors
   module BT = BaseTypes
   module RT = ReturnTypes
@@ -1379,7 +1535,7 @@ module BaseTyping = struct
   type label_context = (AT.lt * Where.label * Locations.t) Sym.Map.t
 
   let check_against_core_bt loc msg2 cbt bt =
-    Typing.lift
+    lift
       (CoreTypeChecks.check_against_core_bt
          (fun msg ->
            Or_TypeError.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) })
@@ -1387,6 +1543,8 @@ module BaseTyping = struct
          bt)
 
 
+  module Mu = Mucore
+
   let rec check_and_bind_pattern bt = function
     | Mu.Pattern (loc, anns, _, p_) ->
       let@ p_ = check_and_bind_pattern_ bt loc p_ in
@@ -1412,8 +1570,7 @@ module BaseTyping = struct
         match BT.is_list_bt bt with
         | Some bt -> return bt
         | None ->
-          fail (fun _ ->
-            { loc; msg = Generic (Pp.item "list pattern match against" (BT.pp bt)) })
+          fail { loc; msg = Generic (Pp.item "list pattern match against" (BT.pp bt)) }
       in
       let@ ctor, pats =
         match (ctor, pats) with
@@ -1421,22 +1578,20 @@ module BaseTyping = struct
           let@ _item_bt = get_item_bt bt in
           return (Mu.Cnil cbt, [])
         | Cnil _, _ ->
-          fail (fun _ ->
-            { loc; msg = Number_arguments { has = List.length pats; expect = 0 } })
+          fail { loc; msg = Number_arguments { has = List.length pats; expect = 0 } }
         | Ccons, [ p1; p2 ] ->
           let@ item_bt = get_item_bt bt in
           let@ p1 = check_and_bind_pattern item_bt p1 in
           let@ p2 = check_and_bind_pattern bt p2 in
           return (Mu.Ccons, [ p1; p2 ])
         | Ccons, _ ->
-          fail (fun _ ->
-            { loc; msg = Number_arguments { has = List.length pats; expect = 2 } })
+          fail { loc; msg = Number_arguments { has = List.length pats; expect = 2 } }
         | Ctuple, pats ->
           let@ bts =
             match BT.is_tuple_bt bt with
             | Some bts when List.length bts == List.length pats -> return bts
             | _ ->
-              fail (fun _ ->
+              fail
                 { loc;
                   msg =
                     Generic
@@ -1444,7 +1599,7 @@ module BaseTyping = struct
                          (Int.to_string (List.length pats)
                           ^ "-length tuple pattern match against")
                          (BT.pp bt))
-                })
+                }
           in
           let@ pats = ListM.map2M check_and_bind_pattern bts pats in
           return (Mu.Ctuple, pats)
@@ -1499,12 +1654,12 @@ module BaseTyping = struct
       if BT.fits_range (Option.get (BT.is_bits_bt bt)) z then
         return (Mu.OV (bt, OVinteger iv))
       else
-        fail (fun _ ->
+        fail
           { loc;
             msg =
               Generic
                 (!^"Value " ^^^ Pp.z z ^^^ !^"does not fit in expected type" ^^^ BT.pp bt)
-          })
+          }
     | _ ->
       let@ ov = infer_object_value loc ov_original in
       let@ () = ensure_base_type loc ~expect:bt (Mu.bt_of_object_value ov) in
@@ -1575,9 +1730,7 @@ module BaseTyping = struct
   let rec infer_pexpr : 'TY. 'TY Mu.pexpr -> BT.t Mu.pexpr m =
     fun pe ->
     let open Mu in
-    Pp.debug
-      22
-      (lazy (Pp.item "WellTyped.BaseTyping.infer_pexpr" (Pp_mucore_ast.pp_pexpr pe)));
+    Pp.debug 22 (lazy (Pp.item __FUNCTION__ (Pp_mucore_ast.pp_pexpr pe)));
     let (Pexpr (loc, annots, _, pe_)) = pe in
     match integer_annot annots with
     | Some ity when !use_ity ->
@@ -1703,8 +1856,8 @@ module BaseTyping = struct
                  let@ () = ensure_base_type loc ~expect:(List ibt) (bt_of_pexpr xs) in
                  return (bt_of_pexpr xs)
                | _ ->
-                 fail (fun _ ->
-                   { loc; msg = Number_arguments { has = List.length pes; expect = 2 } }))
+                 fail
+                   { loc; msg = Number_arguments { has = List.length pes; expect = 2 } })
             | Ctuple -> return (BT.Tuple (List.map bt_of_pexpr pes))
             | Carray ->
               let ibt = bt_of_pexpr (List.hd pes) in
@@ -1796,21 +1949,21 @@ module BaseTyping = struct
         let@ () = ensure_bits_type loc bt in
         return bt
       | None, _ ->
-        fail (fun _ ->
+        fail
           { loc;
             msg =
               Generic
                 (Pp.item "untypeable mucore function" (Pp_mucore_ast.pp_pexpr orig_pe))
-          })
+          }
       | Some `Returns_Integer, None ->
-        fail (fun _ ->
+        fail
           { loc;
             msg =
               Generic
                 (Pp.item
                    "mucore function requires type-annotation"
                    (Pp_mucore_ast.pp_pexpr orig_pe))
-          })
+          }
     in
     return (bt, pexps)
 
@@ -1819,10 +1972,7 @@ module BaseTyping = struct
     let open Cnprog in
     Pp.debug
       22
-      (lazy
-        (Pp.item
-           "WellTyped.check_cn_statement"
-           (CF.Pp_ast.pp_doc_tree (dtree_of_statement stmt))));
+      (lazy (Pp.item __FUNCTION__ (CF.Pp_ast.pp_doc_tree (dtree_of_statement stmt))));
     match stmt with
     | Pack_unpack (pack_unpack, pt) ->
       let@ p_pt = WReq.welltyped loc (P pt) in
@@ -1886,7 +2036,7 @@ module BaseTyping = struct
         let wrong_number_arguments () =
           let has = List.length its in
           let expect = AT.count_computational lemma_typ in
-          fail (fun _ -> { loc; msg = Number_arguments { has; expect } })
+          fail { loc; msg = Number_arguments { has; expect } }
         in
         let rec check_args lemma_typ its =
           match (lemma_typ, its) with
@@ -1935,9 +2085,7 @@ module BaseTyping = struct
   let rec infer_expr : 'TY. label_context -> 'TY Mu.expr -> BT.t Mu.expr m =
     fun label_context e ->
     let open Mu in
-    Pp.debug
-      22
-      (lazy (Pp.item "WellTyped.BaseTyping.infer_expr" (Pp_mucore_ast.pp_expr e)));
+    Pp.debug 22 (lazy (Pp.item __FUNCTION__ (Pp_mucore_ast.pp_expr e)));
     let (Expr (loc, annots, _, e_)) = e in
     match integer_annot annots with
     | Some ity when !use_ity ->
@@ -2062,12 +2210,12 @@ module BaseTyping = struct
               assert (not is_variadic);
               return (snd ret_v_ct, List.map fst arg_r_cts)
             | _ ->
-              fail (fun _ ->
+              fail
                 { loc;
                   msg =
                     Generic
                       (Pp.item "not a function pointer at call-site" (Sctypes.pp act.ct))
-                })
+                }
           in
           let@ f_pe = check_pexpr (Loc ()) f_pe in
           (* TODO: we'd have to check the arguments against the function type, but we
@@ -2116,16 +2264,14 @@ module BaseTyping = struct
           (* copying from check.ml *)
           let@ lt, _lkind =
             match Sym.Map.find_opt l label_context with
-            | None ->
-              fail (fun _ ->
-                { loc; msg = Generic (!^"undefined code label" ^/^ Sym.pp l) })
+            | None -> fail { loc; msg = Generic (!^"undefined code label" ^/^ Sym.pp l) }
             | Some (lt, lkind, _) -> return (lt, lkind)
           in
           let@ pes =
             let wrong_number_arguments () =
               let has = List.length pes in
               let expect = AT.count_computational lt in
-              fail (fun _ -> { loc; msg = Number_arguments { has; expect } })
+              fail { loc; msg = Number_arguments { has; expect } }
             in
             let rec check_args lt pes =
               match (lt, pes) with
@@ -2173,16 +2319,23 @@ module BaseTyping = struct
 end
 
 module WLabel = struct
-  open Mu
+  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
-  open Mu
+  module AT = ArgumentTypes
+  module LAT = LogicalArgumentTypes
+  module Mu = Mucore
+  open Mucore
 
   let label_context function_rt label_defs =
     Pmap.fold
@@ -2205,9 +2358,42 @@ module WProc = struct
 
   let typ p = WArgs.typ (fun (_body, _labels, rt) -> rt) p
 
+  let consistent : Loc.t -> _ Mu.args_and_body -> unit m =
+    fun (loc : Loc.t) (at : 'TY1 Mu.args_and_body) ->
+    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
+            | Return _ -> return ()
+            | Label (loc, label_args_and_body, _annots, _parsed_spec, _loop_info) ->
+              pure_and_no_initial_resources
+                loc
+                (WArgs.consistent
+                   (fun _loc _label_body -> return ())
+                   "label"
+                   loc
+                   label_args_and_body))
+          labels)
+      "function"
+      loc
+      at
+
+
   let welltyped : Loc.t -> _ Mu.args_and_body -> _ Mu.args_and_body m =
     fun (loc : Loc.t) (at : 'TY1 Mu.args_and_body) ->
-    Pp.(debug 6 (lazy !^__LOC__));
     WArgs.welltyped
       (fun loc (body, labels, rt) ->
         let@ rt = pure_and_no_initial_resources loc (WRT.welltyped loc rt) in
@@ -2255,6 +2441,45 @@ module WProc = struct
 end
 
 module WRPD = struct
+  module Def = Definition
+  module LC = LogicalConstraints
+
+  let consistent Def.Predicate.{ loc; pointer; iargs; oarg_bt = _; clauses } =
+    let open Typing in
+    (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
+    pure
+      (let@ () = add_l pointer BT.(Loc ()) (loc, lazy (Pp.string "ptr-var")) in
+       let@ () =
+         ListM.iterM (fun (s, bt) -> add_l s bt (loc, lazy (Pp.string "input-var"))) iargs
+       in
+       match clauses with
+       | None -> return ()
+       | Some clauses ->
+         let@ _ =
+           ListM.fold_leftM
+             (fun acc Def.Clause.{ loc; guard; packing_ft } ->
+               let here = Locations.other __LOC__ in
+               let negated_guards =
+                 List.map (fun clause -> IT.not_ clause.Def.Clause.guard here) acc
+               in
+               pure
+                 (let@ () = add_c loc (LC.T guard) in
+                  let@ () = add_c loc (LC.T (IT.and_ negated_guards here)) in
+                  let@ () =
+                    WLAT.consistent
+                      (fun _loc _it -> return ())
+                      IT.pp
+                      "clause"
+                      loc
+                      packing_ft
+                  in
+                  return (acc @ [ Def.Clause.{ loc; guard; packing_ft } ])))
+             []
+             clauses
+         in
+         return ())
+
+
   let welltyped Def.Predicate.{ loc; pointer; iargs; oarg_bt; clauses } =
     (* no need to alpha-rename, because context.ml ensures there's no name clashes *)
     pure
@@ -2276,14 +2501,8 @@ module WRPD = struct
              ListM.fold_leftM
                (fun acc Def.Clause.{ loc; guard; packing_ft } ->
                  let@ guard = WIT.check loc BT.Bool guard in
-                 let here = Locations.other __LOC__ in
-                 let negated_guards =
-                   List.map (fun clause -> IT.not_ clause.Def.Clause.guard here) acc
-                 in
                  pure
-                   (let@ () = add_c loc (LC.T guard) in
-                    let@ () = add_c loc (LC.T (IT.and_ negated_guards here)) in
-                    let@ packing_ft =
+                   (let@ packing_ft =
                       WLAT.welltyped
                         (fun loc it -> WIT.check loc oarg_bt it)
                         IT.pp
@@ -2329,17 +2548,26 @@ module WLFD = struct
 end
 
 module WLemma = struct
+  let consistent loc _lemma_s lemma_typ =
+    WAT.consistent
+      (fun loc lrt -> pure_and_no_initial_resources loc (WLRT.consistent loc lrt))
+      LogicalReturnTypes.pp
+      "lemma"
+      loc
+      lemma_typ
+
+
   let welltyped loc _lemma_s lemma_typ =
     WAT.welltyped
       (fun loc lrt -> pure_and_no_initial_resources loc (WLRT.welltyped loc lrt))
-      LRT.pp
+      LogicalReturnTypes.pp
       "lemma"
       loc
       lemma_typ
 end
 
 module WDT = struct
-  open Mu
+  open Mucore
 
   let welltyped (dt_name, { loc; cases }) =
     let@ _ =
@@ -2434,7 +2662,7 @@ module WDT = struct
                           ^/^ !^"Indirect recursion via map, set, record,"
                           ^^^ !^"or tuple types is not permitted."
                         in
-                        fail (fun _ -> { loc; msg = Generic err }))
+                        fail { loc; msg = Generic err })
                     args)
                 cases)
             scc)
diff --git a/tests/cn/implies3.error.c.verify b/tests/cn/implies3.error.c.verify
index 6958a7939..2d7b1bede 100644
--- a/tests/cn/implies3.error.c.verify
+++ b/tests/cn/implies3.error.c.verify
@@ -1,5 +1,5 @@
 return code: 1
-tests/cn/implies3.error.c:1:1: error: function makes inconsistent assumptions
+tests/cn/implies3.error.c:1:1: error: proc/fun makes inconsistent assumptions
 int foo ()
 ~~~~^~~~~~ 
 State file: file:///tmp/state__implies3.error.c.html
diff --git a/tests/cn/inconsistent.error.c.verify b/tests/cn/inconsistent.error.c.verify
index 29136eb38..d0a2acb96 100644
--- a/tests/cn/inconsistent.error.c.verify
+++ b/tests/cn/inconsistent.error.c.verify
@@ -1,5 +1,5 @@
 return code: 1
-tests/cn/inconsistent.error.c:1:1: error: function makes inconsistent assumptions
+tests/cn/inconsistent.error.c:1:1: error: proc/fun makes inconsistent assumptions
 void f()
 ~~~~~^~~ 
 State file: file:///tmp/state__inconsistent.error.c.html
diff --git a/tests/cn/inconsistent2.error.c.verify b/tests/cn/inconsistent2.error.c.verify
index 125c67455..845303060 100644
--- a/tests/cn/inconsistent2.error.c.verify
+++ b/tests/cn/inconsistent2.error.c.verify
@@ -2,6 +2,9 @@ return code: 1
 tests/cn/inconsistent2.error.c:9:19: warning: 'each' expects a 'u64', but 'i' with type 'i32' was provided. This will become an error in the future.
 /*@ requires take f1 = each(i32 i; 0i32 <= i && i <= 0i32) { False(p + i, i) };
                   ^
+tests/cn/inconsistent2.error.c:12:22: warning: 'extract' expects a 'u64', but '0'i32' with type 'i32' was provided. This will become an error in the future.
+  /*@ extract False, 0i32; @*/
+                     ^
 tests/cn/inconsistent2.error.c:8:1: error: return type makes inconsistent assumptions
 void f (int *p)
 ~~~~~^~~~~~~~~~