anchor.diff:    | Construct of fv * list<universe> * list<(t * aqual)> (* Zoe: This is used for both type and data constructors*)
     | Unit
     | Bool of bool
  +  | Univ of universe
   
   type head = t
   type annot = option<t>
  
positive.code: 
      | Construct (fv, us, args) ->
        let args = map_rev (fun (x, q) -> (readback env x, q)) args in
        (match args with
         | [] -> (S.mk (Tm_fvar fv) None Range.dummyRange)
         | _ ->
           (match us with
            | u::us -> U.mk_app (S.mk_Tm_uinst (S.mk (Tm_fvar fv) None Range.dummyRange) (u::us)) args
            | [] -> U.mk_app (S.mk (Tm_fvar fv) None Range.dummyRange) args))
  
      | Accu (Var bv, []) ->
        S.bv_to_name bv
  
negative.code:        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 env (curry (translate_letbinding env ((mkAccuRec lb bs) :: bs) lb) 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? *)
  