anchor.diff:      let env = instantiate_both env in
       match top.n with
           | Tm_let((true, lbs), e2) ->
  +           (* replace bound variables in terms and of universes with new names (free variables) *)
   (*open*)   let lbs, e2 = SS.open_let_rec lbs e2 in
   
  +           (* expected types for top level definitions are stored in the lbs and we therefore just
  +            * remove previous, unrelated, expected type in env
  +            * the expected type is defined within lbs
  +            * *)
              let env0, topt = Env.clear_expected_typ env in
              let lbs, rec_env = build_let_rec_env true env0 lbs in
  +           (* now we type check each let rec *)
              let lbs, g_lbs = check_let_recs rec_env lbs in
              let g_lbs = Rel.solve_deferred_constraints env g_lbs |> Rel.resolve_implicits in
   
  
positive.code:     value_check_expected_typ env0 e (Inl t) g
  
    | Tm_abs(bs, body, _) ->
      let bs = TcUtil.maybe_add_implicit_binders env bs in
      if Env.debug env Options.Low
      then BU.print1 "Abstraction is: %s\n" (Print.term_to_string ({top with n=Tm_abs(bs, body, None)}));
  
negative.code:           as_function_typ false t
      in
  
      (* whether to try first to use unification for solving sub-typing constraints or only propagate to the SMT solver *)
      let use_eq = env.use_eq in
      (* topt is the expected type of the expression obtained from the env *)
      let env, topt = Env.clear_expected_typ env in
  
      if Env.debug env Options.High
  