anchor.diff:      | pat, None, body ->
           let env = { env with env = List.fold_left push_bv env.env (pat_bvs pat) } in
           let nm, s_body, u_body = f env body in
  -        nm, (Util.must <| strip_implicits pat, None, (s_body, u_body))
  +        nm, (pat, None, (s_body, u_body, body))
       | _ ->
           raise (Err ("No when clauses in the definition language"))
     ) branches) in
     let t1 = match List.hd nms with | M t1 | N t1 -> t1 in
     let has_m = List.existsb (function | M _ -> true | _ -> false) nms in
  -  let nms, s_branches, u_branches = List.unzip3 (List.map2 (fun nm (pat, guard, (s_body, u_body)) ->
  +  let nms, s_branches, u_branches = List.unzip3 (List.map2 (fun nm (pat, guard, (s_body, u_body, original_body)) ->
       match nm, has_m with
       | N t2, false
       | M t2, true ->
           nm, (pat, guard, s_body), (pat, guard, u_body)
       | N t2, true ->
  -        // TODO: we could re-generate the body of the branch with [check_m] and
  -        // have [return]s inserted at depth, rather than on the outside...
  -        M t2, (pat, guard, mk_return env t2 s_body), (pat, guard, u_body)
  +        // In checking mode, all the branches are run through "check"... meaning
  +        // that they're either all N or all M... the lift from N to M can only
  +        // occur in infer mode... instead of calling [mk_return s_body],
  +        // re-check_m everything and get code that's better for z3
  +        let _, s_body, u_body = check env original_body (M t2) in
  +        M t2, (pat, guard, s_body), (pat, guard, u_body)
       | M _, false ->
           failwith "impossible"
     ) nms branches) in
     let s_branches = List.map close_branch s_branches in
     let u_branches = List.map close_branch u_branches in
  -  let t1_star = 
  -    if has_m 
  -    then U.arrow [S.mk_binder <| S.new_bv None (mk_star_to_type mk env t1)] (S.mk_Total U.ktype0)
  -    else t1 in
  +  let t1_star =
  +    if has_m then
  +      U.arrow [S.mk_binder <| S.new_bv None (mk_star_to_type mk env t1)] (S.mk_Total U.ktype0)
  +    else
  +      t1
  +  in
     (if has_m then M t1 else N t1), 
     mk (Tm_ascribed (mk (Tm_match (s_e0, s_branches)), Inl t1_star, None)),
     mk (Tm_match (u_e0, u_branches))
  
positive.code: 
    in
  
    match (SS.compress e).n with
    | Tm_bvar _
    | Tm_name _
  
negative.code:         (fun env e2 -> check env e2 context_nm)
          // Body of the let is monadic: this is a bind, and we must strengthen
          // the check on the continuation to ensure it is a monadic computation
          ensure_m
  
    | Tm_match (e0, branches) ->
        // This is similar to the [let] case above. The [match] checks that the
  