anchor.diff:      | letrecs ->
         let r = Env.get_range env in
         let env = {env with letrecs=[]} in
  -      let precedes = TcUtil.fvar_const env Const.precedes_lid in
   
         let decreases_clause bs c =
             if debug env Options.Low
  
positive.code:         //make sure they all have non-null names
          let formals = formals |> List.map (fun (x, imp) -> if S.is_null_bv x then (S.new_bv (Some (S.range_of_bv x)) x.sort, imp) else x,imp) in
          let dec = decreases_clause formals c in
          let precedes = mk_Tm_app precedes [as_arg dec; as_arg previous_dec] r in
          let precedes = TcUtil.label "Could not prove termination of this recursive call" r precedes in
          let bs, (last, imp) = BU.prefix formals in
          let last = {last with sort=U.refine last precedes} in
  
negative.code:       let _, args = U.head_and_args tc in
        let res, args = List.hd args, List.tl args in
        let flags, guards = c.flags |> List.map (function
          | DECREASES l ->
              let env, _ = Env.clear_expected_typ env in
              let l, g = l |> List.fold_left (fun (l, g) e ->
                let e, _, g_e = tc_tot_or_gtot_term env e in
                l@[e], Env.conj_guard g g_e) ([], Env.trivial_guard) in
              DECREASES l, g
          | f -> f, Env.trivial_guard) |> List.unzip in
        let u = env.universe_of env (fst res) in
        let c = mk_Comp ({c with
  