anchor.diff:      | Accu (Var bv, ts) ->
         let args = map_rev (fun x -> as_arg (readback x)) ts in
         U.mk_app (S.bv_to_name bv) args
  +    | Accu (Type u, []) ->
  +      S.mk (Tm_type u) None Range.dummyRange
  +    | Accu (Type u, ts) ->
  +      let args = map_rev (fun x -> as_arg (readback x)) ts in
  +      U.mk_app (S.mk (Tm_type u) None Range.dummyRange) args
       | Accu (Match (scrut, cases), ts) ->
         let args = map_rev (fun x -> as_arg (readback x)) ts in
         let head =  readback (cases scrut) in
  
positive.code: let mkAccuVar (v:var) = Accu(Var v, [])
  let mkAccuMatch (s : t) (c : t -> t) = Accu(Match (s, c), [])
  let mkAccuRec (b:letbinding) (env:list<t>) = Accu(Rec(b, env), [])
  
  let isAccu (trm:t) = 
    match trm with 
  
negative.code: 
      | Tm_uinst _ -> debug_term e; failwith "Tm_uinst: Not yet implemented"
  
      | Tm_type u -> mkAccTyp u
  
      | Tm_arrow (bs, c) -> debug_term e; failwith "Tm_arrow: Not yet implemented"
  
  