anchor.diff:         let args_no = count_abstractions lb.lbdef in 
          // Printf.printf "Args no. %d\n" args_no;
          if test_args ts args_no then (* if the arguments are not symbolic and the application is not partial compute *)
  -         readback (curry (translate ((mkAccuRec lb bs) :: bs) lb.lbdef) ts)
  +         readback env (curry (translate env ((mkAccuRec lb bs) :: bs) lb.lbdef) ts)
          else (* otherwise do not unfold *)
            let head = 
              (* Zoe: I want the head to be [let rec f = lb in f]. Is this the right way to construct it? *)
  
positive.code:            in
             S.mk (Tm_let((true, [lb]), f)) None Range.dummyRange
           in
           let args = map_rev (fun x -> as_arg (readback x)) ts in
           (match ts with 
            | [] -> head
            | _ -> U.mk_app head args)
  
negative.code: module U = FStar.Syntax.Util
  module P = FStar.Syntax.Print
  module BU = FStar.Util
  module Env = FStar.TypeChecker.Env
  
  (* Utils *)
  
  