anchor.diff:        let n = List.length univs in
         let n_binders = List.length binders in
         let elim_tscheme (us, t) =
  -//        printfn "0. elim_tscheme %s" (Print.tscheme_to_string (us, t));
           let n_us = List.length us in
           let us, t = SS.open_univ_vars us t in
  -//        printfn "1. elim_tscheme %s" (Print.tscheme_to_string (us, t));
           let b_opening, b_closing =
               b_opening |> SS.shift_subst n_us,
               b_closing |> SS.shift_subst n_us in
           let univs_opening, univs_closing =
               univs_opening |> SS.shift_subst n_us,
               univs_closing |> SS.shift_subst n_us in
  -//        let opening = univs_opening @ b_opening in
  -//        printfn "univs_opening = %A" univs_opening;
           let t = SS.subst univs_opening (SS.subst b_opening t) in
  -//        printfn "2. elim_tscheme opened to %s" (Print.term_to_string t);
           let _, _, t = elim_uvars_aux_t env [] [] t in
           let t = SS.subst univs_closing (SS.subst b_closing (SS.close_univ_vars us t)) in
           us, t
  
positive.code:                     let t = mk (Tm_meta(head, m)) t.pos in
                      rebuild cfg env stack t
                  end
          end
  
  and do_unfold_fv cfg env stack (t0:term) (f:fv) : term =
      //preserve the range info on the returned def
  
negative.code:       end
  
  //////////////////////////////////////////////////////////////////
  //Eliminating all unification variables and delayed substitutions in a sigelt
  //////////////////////////////////////////////////////////////////
  
  let rec elim_delayed_subst_term (t:term) : term =
      let mk x = S.mk x None t.pos in
      let t = SS.compress t in
      let elim_bv x = {x with sort=elim_delayed_subst_term x.sort} in
      match t.n with
      | Tm_delayed _ -> failwith "Impossible"
      | Tm_bvar _
      | Tm_name _
      | Tm_fvar _
      | Tm_uinst _
      | Tm_constant _
      | Tm_type _
      | Tm_unknown -> t
  
      | Tm_abs(bs, t, rc_opt) ->
        let elim_rc rc =
          {rc with
              residual_typ=BU.map_opt rc.residual_typ elim_delayed_subst_term;
              residual_flags=elim_delayed_subst_cflags rc.residual_flags}
        in
        mk (Tm_abs(elim_delayed_subst_binders bs,
                   elim_delayed_subst_term t,
                   BU.map_opt rc_opt elim_rc))
  
      | Tm_arrow(bs, c) ->
        mk (Tm_arrow(elim_delayed_subst_binders bs, elim_delayed_subst_comp c))
  
      | Tm_refine(bv, phi) ->
        mk (Tm_refine(elim_bv bv, elim_delayed_subst_term phi))
  
      | Tm_app(t, args) ->
        mk (Tm_app(elim_delayed_subst_term t, elim_delayed_subst_args args))
  
      | Tm_match(t, branches) ->
        let rec elim_pat (p:pat) =
          match p.v with
          | Pat_var x ->
            {p with v=Pat_var (elim_bv x)}
          | Pat_wild x ->
            {p with v=Pat_wild (elim_bv x)}
          | Pat_dot_term(x, t0) ->
            {p with v=Pat_dot_term(elim_bv x, elim_delayed_subst_term t0)}
          | Pat_cons (fv, pats) ->
            {p with v=Pat_cons(fv, List.map (fun (x, b) -> elim_pat x, b) pats)}
          | _ -> p
        in
        let elim_branch (pat, wopt, t) =
            (elim_pat pat,
             BU.map_opt wopt elim_delayed_subst_term,
             elim_delayed_subst_term t)
        in
        mk (Tm_match(elim_delayed_subst_term t, List.map elim_branch branches))
  
      | Tm_ascribed(t, a, lopt) ->
        let elim_ascription (tc, topt) =
          (match tc with
           | Inl t -> Inl (elim_delayed_subst_term t)
           | Inr c -> Inr (elim_delayed_subst_comp c)),
          BU.map_opt topt elim_delayed_subst_term
        in
        mk (Tm_ascribed(elim_delayed_subst_term t, elim_ascription a, lopt))
  
      | Tm_let(lbs, t) ->
        let elim_lb lb =
           {lb with
               lbtyp = elim_delayed_subst_term lb.lbtyp;
               lbdef = elim_delayed_subst_term lb.lbdef }
        in
        mk (Tm_let((fst lbs, List.map elim_lb (snd lbs)),
                    elim_delayed_subst_term t))
  
      | Tm_uvar(uv, t) ->
        mk (Tm_uvar(uv, elim_delayed_subst_term t))
  
      | Tm_meta(t, md) ->
        mk (Tm_meta(elim_delayed_subst_term t, elim_delayed_subst_meta md))
  
  and elim_delayed_subst_cflags flags =
      List.map
          (function
          | DECREASES t -> DECREASES (elim_delayed_subst_term t)
          | f -> f)
          flags
  
  and elim_delayed_subst_comp (c:comp) : comp =
      let mk x = S.mk x None c.pos in
      match c.n with
      | Total(t, uopt) ->
        mk (Total(elim_delayed_subst_term t, uopt))
      | GTotal(t, uopt) ->
        mk (GTotal(elim_delayed_subst_term t, uopt))
      | Comp ct ->
        let ct =
          {ct with
              result_typ=elim_delayed_subst_term ct.result_typ;
              effect_args=elim_delayed_subst_args ct.effect_args;
              flags=elim_delayed_subst_cflags ct.flags} in
        mk (Comp ct)
  
  and elim_delayed_subst_meta = function
    | Meta_pattern args -> Meta_pattern(List.map elim_delayed_subst_args args)
    | Meta_monadic(m, t) -> Meta_monadic(m, elim_delayed_subst_term t)
    | Meta_monadic_lift(m1, m2, t) -> Meta_monadic_lift(m1, m2, elim_delayed_subst_term t)
    | Meta_alien(d, s, t) -> Meta_alien(d, s, elim_delayed_subst_term t)
    | m -> m
  
  and elim_delayed_subst_args args =
      List.map (fun (t, q) -> elim_delayed_subst_term t, q) args
  
  and elim_delayed_subst_binders bs =
      List.map (fun (x, q) -> {x with sort=elim_delayed_subst_term x.sort}, q) bs
  
  let elim_uvars_aux_tc (env:Env.env) (univ_names:univ_names) (binders:binders) (tc:either<typ, comp>) =
      let t =
        match binders, tc with
  