anchor.diff:                                  term)
                   else term in 
               term,
  +            exclude_cvars bs (cvars@cvars'),
               decls@decls'
   
           | _ -> failwith (Util.format1 "Unknown kind: %s" (Print.kind_to_string k))
   
   and encode_knd (k:knd) (env:env_t) (t:term) = encode_knd' true k env t
   
  -and encode_binders (fuel_opt:option<term>) (bs:Syntax.binders) (env:env_t) : (list<var>       (* translated bound variables *)
  -                                                      * list<term>    (* guards *)
  -                                                      * env_t         (* extended context *)
  -                                                      * decls_t         (* top-level decls to be emitted *)
  -                                                      * list<either<btvdef, bvvdef>>) (* unmangled names *) =
  +and encode_binders (fuel_opt:option<term>) (bs:Syntax.binders) (env:env_t) : 
  +                            (list<var>                      (* translated bound variables *)
  +                            * closure_vars
  +                            * list<term>                    (* guards *)
  +                            * env_t                         (* extended context *)
  +                            * decls_t                       (* top-level decls to be emitted *)
  +                            * list<either<btvdef, bvvdef>>) (* unmangled names *) =
   
       if Tc.Env.debug env.tcenv Options.Low then Util.fprint1 "Encoding binders %s\n" (Print.binders_to_string ", " bs);
       
  -    let vars, guards, env, decls, names = bs |> List.fold_left (fun (vars, guards, env, decls, names) b -> 
  -        let v, g, env, decls', n = match fst b with 
  +    let vars, cvars, guards, env, decls, names = bs |> List.fold_left (fun (vars, cvars, guards, env, decls, names) b -> 
  +        let v, cvars', g, env, decls', n = match fst b with 
               | Inl {v=a; sort=k} -> 
                   let a = unmangle a in
                   let aasym, aa, env' = 
                       if is_null_binder b 
                       then withenv env <| fresh_bvar "a" Type_sort
                       else gen_typ_var env a in 
  -                let guard_a_k,decls' = encode_knd' false k env aa in
  +                let guard_a_k, cvars, decls' = encode_knd' false k env aa in
                   (aasym, Type_sort), 
  +                cvars,
                   guard_a_k,
                   env', 
                   decls',
  
positive.code:     | Binding_tvar  of btvdef * term
      | Binding_fvar  of lident * string * term * option<term> (* free variables, depending on whether or not they are fully applied ...  *)
      | Binding_ftvar of lident * string * term (* ... are mapped either to SMT2 functions, or to nullary term/type tokens *)
     
  type env_t = {bindings:list<binding>;
                tcenv:Env.env;
                warn:bool;
  
negative.code:               encode_typ_term t env
          end
  
        | 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
  