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: //IN F*: type atom : Type0 =
  type atom = //JUST FSHARP
    | Var of var
    | Sort of sort (* for full CiC -- not used right now *)
    | Prod of t * t (* for full CiC -- not used right now *)
    | Match of t * (* the scutinee *)
               (t -> t) (* the closure that pattern matches the scrutiny *) 
    | Rec of letbinding * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
  //IN F*: and t : Type0 =
  and t = //JUST FSHARP
    | Lam of (t -> t)
    | Fix of (t -> t) (* potentially recursive (i.e. a lambda inside ). The only difference with [Lam] is that there is an [is_accu] for the argument during application *)
    | Accu of atom * list<t>
    (* For simplicity represent constructors with fv as in F* *)
    | Construct of fv * list<t>
  
negative.code: //                      only normalizing it when it is unfolded *)
  //         | _ -> failwith "Recursive definition not a function")
  // >>>>>>> 86f93ae6edc257258f376954fed7fba11f53ff83
  
  let normalize (e:term) : term = readback (translate [] e)
  