anchor.diff:    let rec make_univ_abst (us:list<univ_name>) (bs:list<t>) (def:term) : t =
       match us with
       | [] -> translate env bs def
  -    | u :: us' -> Lam ((fun u -> make_univ_abst us' (u :: bs) def), None) // Zoe: Leaving universe binder qualifier none for now; NS: makes sense
  +      | u :: us' -> Lam ((fun u -> make_univ_abst us' (u :: bs) def), Constant Unit, None) // Zoe: Bogus type! The idea is that we will never readback these lambdas
     in
     make_univ_abst lb.lbunivs bs lb.lbdef
   
  
positive.code:     | Type_t u ->
        S.mk (Tm_type u) None Range.dummyRange
  
      | Lam (f, q) ->
        let x = S.new_bv None S.tun in
        let body = readback env (f (mkAccuVar x)) in
        U.abs [(x, q)] body None
  
  
negative.code: 
      | Tm_abs ([x], body, _) ->
        debug (fun () -> BU.print2 "Tm_abs body : %s - %s\n" (P.tag_of_term body) (P.term_to_string body));
        let x1 = fst x in
        Lam ((fun (y:t) -> translate env (y::bs) body), translate env bs x1.sort, snd x)
  
      | Tm_abs (x::xs, body, _) ->
        let rest = S.mk (Tm_abs(xs, body, None)) None Range.dummyRange in
  