anchor.diff:        (match args with 
          | [] -> (S.mk (Tm_fvar fv) None Range.dummyRange)
          | _ -> U.mk_app (S.mk (Tm_fvar fv) None Range.dummyRange) args)
  -    
  +      
       | Accu (Var bv, []) ->
         S.bv_to_name bv
       | Accu (Var bv, ts) ->
  
positive.code:     | Accu (Type u, ts) ->
        let args = map_rev (fun x -> as_arg (readback env x)) ts in
        U.mk_app (S.mk (Tm_type u) None Range.dummyRange) args
     
      | Accu (Inductive fv, []) ->
        S.mk (Tm_fvar fv) None Range.dummyRange
      | Accu (Inductive fv, ts) ->
        let args = map_rev (fun x -> as_arg (readback env x)) ts in
        U.mk_app (S.mk (Tm_fvar fv) None Range.dummyRange) args
        
      | Accu (Match (scrut, cases), ts) ->
        let args = map_rev (fun x -> as_arg (readback env x)) ts in
        let head =  readback env (cases scrut) in
  
negative.code: //         | _ -> failwith "Recursive definition not a function")
  // >>>>>>> 86f93ae6edc257258f376954fed7fba11f53ff83
  
  let normalize (env : Env.env) (e:term) : term = 
    //debug_sigmap env.sigtab;
    readback env (translate env [] e)
  