anchor.diff:  let mkAccuMatch (s : t) (c : t -> t) = Accu(Match (s, c), [])
   let mkAccuRec (b:letbinding) (env:list<t>) = Accu(Rec(b, env), [])
   let mkAccTyp (u:universe) = Accu(Type u, [])
  +let mkAccInd (fvar : fv) = Accu(Inductive fvar, [])
   
   let isAccu (trm:t) = 
     match trm with 
  
positive.code: and readback (env:Env.env) (x:t) : term =
      match x with
      | Unit -> S.unit_const
      | Bool true -> U.exp_true_bool
      | Bool false -> U.exp_false_bool
      | Lam f ->
        let x = S.new_bv None S.tun in
        let body = readback env (f (mkAccuVar x)) in
        U.abs [S.mk_binder x] body None
      | Construct (fv, args) -> 
        let args = List.map (fun x -> as_arg (readback env x)) args in
        (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) ->
        let args = map_rev (fun x -> as_arg (readback env 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 env 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 env x)) ts in
        let head =  readback env (cases scrut) in
        (match ts with 
         | [] -> head
         | _ -> U.mk_app head args)
      | Accu (Rec(lb, bs), ts) ->
         let rec curry hd args = 
         match args with 
  
negative.code:     | Tm_abs ([x], body, _) ->
        Lam (fun (y:t) -> translate env (y::bs) body)
  
      | Tm_fvar fvar ->
        let find_in_sigtab (env : Env.env) (lid : lident) : option<sigelt> = BU.smap_try_find env.sigtab (text_of_lid lid) in
        (match find_in_sigtab env fvar.fv_name.v with 
         | Some elt ->
           (match elt.sigel with 
            | Sig_datacon _ -> mkConstruct fvar []
            | Sig_inductive_typ _ -> mkAccInd fvar
            | _ -> failwith "Sigelt not yet supported")
         | None -> failwith "Free variable not found")
      | Tm_abs (x::xs, body, _) ->
        let rest = S.mk (Tm_abs(xs, body, None)) None Range.dummyRange in
        let tm = S.mk (Tm_abs([x], rest, None)) None e.pos in
  