anchor.diff:                encode_typ_term t env
           end
   
  -      | Typ_lam(bs, t) ->
  -        let vars, guards, env, decls, _ = encode_binders None bs env in
  -        let name = varops.fresh (Print.tag_of_typ t0), Type_sort in 
  -        let tag = mkBoundV name in 
  -        let ktm, decls'' = encode_knd (Tc.Recheck.recompute_kind t0) env tag in
  -        let app = mk_ApplyT tag vars in
  -        let body, vars_body, decls' = encode_typ_term t env in
  -        let eq = close_ex vars_body (mkEq(app, body)) in
  -        let guard = mkForall([app], vars, mkImp(mk_and_l guards, eq)) in
  -        tag, [(name, Term.mkAnd(ktm, guard))], decls@decls''@decls'
  +      | Typ_lam(bs, body) ->
  +        let vars, cvars, guards, env, decls, _ = encode_binders None bs env in
  +        let body, cvars', decls' = encode_typ_term body env in
  +        
  +        let cvars = exclude_cvars bs (cvars@cvars') in
  +      
  +        let tsym = varops.fresh "Typ_lam" in
  +        let tdecl = Term.DeclFun(tsym, cvar_sorts cvars, Type_sort, None) in
  +        let t = Term.mkApp(tsym, cvar_terms cvars) in
  +
  +        let app = mk_ApplyT t vars in
  +        let interp = Term.Assume(mkForall([app], vars@cvar_binders cvars, mkImp(mk_and_l guards, mkEq(app,body))), 
  +                                 Some "Typ_lam interpretation") in
  +        let kinding =    
  +            let ktm, _, decls'' = encode_knd (Tc.Recheck.recompute_kind t0) env t in
  +            decls''@[Term.Assume(mkForall([t], cvar_binders cvars, ktm), Some "Typ_lam kinding")] in
  +
  +        t, cvars, decls@decls'@interp::kinding
   
         | Typ_ascribed(t, _) -> 
           encode_typ_term t env
  
positive.code:             close_ex ex (mk_HasTypeWithFuel fuel_opt e t), decls
  
  and encode_typ_term (t:typ) (env:env_t) : (term       (* encoding of t, expects t to be in normal form already *)
                                             * ex_vars  (* new names and guards generated for this type, which must be bound in the caller's scope *)
                                             * decls_t)   (* top-level declarations to be emitted (for shared representations of existentially bound terms *) = 
      let fresh_vars tname xname = 
          let tsym = varops.fresh tname, Type_sort in
          let ttm = mkBoundV tsym in
  
negative.code:                     if is_null_binder b   
                      then withenv env <| fresh_bvar "x" Term_sort
                      else gen_term_var env x in
                  let guard_x_t, cvars, decls' = encode_typ_pred' fuel_opt (norm_t env t) env xx in
                  (xxsym, Term_sort),
                  cvars, 
                  guard_x_t,
                  env', 
                  decls',
                  Inr x in
          v::vars, cvars@cvars', g::guards, env, decls@decls', n::names) ([], [], [], env, [], []) in
      List.rev vars,
      cvars,
      List.rev guards,
      env, 
      decls,
      List.rev names
  
  and encode_typ_pred' (fuel_opt:option<term>) (t:typ) (env:env_t) (e:term) : term * closure_vars * decls_t = 
      let t = Util.compress_typ t in 
      match (Util.unmeta_typ t).n with 
          | Typ_refine(x, f) -> 
  