type nat =
  | O
  | S of nat

type 'a list =
  | Nil
  | Cons of 'a * 'a list

type 'dom var =
  | First of 'dom list * 'dom
  | Next of 'dom list * 'dom * 'dom * 'dom var

(** val varConvert : ('a1 -> 'a2) -> 'a1 list -> 'a1 -> 'a1 var -> 'a2 var **)

let rec varConvert convert g t = function
  | First (g0, t0) -> First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t1) -> Cons ((convert a), (map t1))
        in map g0), (convert t0))
  | Next (g0, t0, t', v') -> Next
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t1) -> Cons ((convert a), (map t1))
        in map g0), (convert t0), (convert t'),
      (varConvert convert g0 t0 v'))

type dty =
  | Nat
  | Prod of dty * dty
  | Sum of dty * dty

type ty =
  | Data of dty
  | Arrow of ty * ty

type term =
  | EVar of ty list * ty * ty var
  | Lam of ty list * ty * ty * term
  | App of ty list * ty * ty * term * term
  | Const of ty list * nat
  | Pair of ty list * dty * dty * term * term
  | Fst of ty list * dty * dty * term
  | Snd of ty list * dty * dty * term
  | Inl of ty list * dty * dty * term
  | Inr of ty list * dty * dty * term
  | Case of ty list * dty * dty * ty * term * term * term

type idty =
  | IUnit
  | INat

type ity =
  | IData of idty
  | IArrow of ity * ity

type iterm =
  | IVar of ity list * ity * ity var
  | ILam of ity list * ity * ity * iterm
  | IApp of ity list * ity * ity * iterm * iterm
  | IUnitE of ity list
  | IConst of ity list * nat
  | ISucc of ity list * iterm
  | IWrite of ity list * iterm * iterm
  | IRead of ity list * iterm
  | ISeq of ity list * ity * iterm * iterm
  | IIf of ity list * ity * iterm * iterm * iterm

(** val compile_ty : ty -> ity **)

let rec compile_ty = function
  | Data d -> IData INat
  | Arrow (t1, t2) -> IArrow ((compile_ty t1), (compile_ty t2))

(** val compile_term : ty list -> ty -> term -> iterm **)

let rec compile_term g t = function
  | EVar (g0, t0, v) -> IVar
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t1) -> Cons ((compile_ty a), (map t1))
        in map g0), (compile_ty t0), (varConvert compile_ty g0 t0 v))
  | Lam (g0, dom, ran, e') -> ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (compile_ty dom), (compile_ty ran),
      (compile_term (Cons (dom, g0)) ran e'))
  | App (g0, dom, ran, e1, e2) -> IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0),
      (let rec compile_ty0 = function
         | Data d -> IData INat
         | Arrow (t1, t2) -> IArrow ((compile_ty0 t1), (compile_ty0 t2))
       in compile_ty0 dom),
      (let rec compile_ty0 = function
         | Data d -> IData INat
         | Arrow (t1, t2) -> IArrow ((compile_ty0 t1), (compile_ty0 t2))
       in compile_ty0 ran), (compile_term g0 (Arrow (dom, ran)) e1),
      (compile_term g0 dom e2))
  | Const (g0, n) -> IConst
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), n)
  | Pair (g0, t1, t2, e1, e2) -> IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IData INat), (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IData INat))),
      (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IArrow ((IData
      INat), (IData INat))))), (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IArrow ((IData
      INat), (IData INat))))), (ILam ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IArrow ((IData INat), (IData INat))),
      (ILam ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IData INat), (ISeq ((Cons ((IData
      INat), (Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (First ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat))))))), (IVar ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (Next ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IData INat), (Next ((Cons ((IData
      INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IData INat), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat))))))))))), (ISeq ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (First ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat))))))))), (IVar ((Cons ((IData INat),
      (Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (Next ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IData INat), (First ((Cons ((IData
      INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))), (ISeq ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IConst ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), O)), (ISucc ((Cons ((IData INat), (Cons ((IData
      INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (First ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat))))))))))), (IVar ((Cons ((IData INat),
      (Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))))), (IData INat), (First ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat))))))))))))))))),
      (compile_term g0 (Data t1) e1))), (compile_term g0 (Data t2) e2))),
      (IRead
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IConst
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), O)))))
  | Fst (g0, t1, t2, e1) -> IRead
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (ISucc
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (compile_term g0 (Data (Prod (t1, t2))) e1))))
  | Snd (g0, t1, t2, e1) -> IRead
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (ISucc
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (ISucc
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (compile_term g0 (Data (Prod (t1, t2))) e1))))))
  | Inl (g0, t1, t2, e1) -> IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IData INat), (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IData INat))),
      (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IData INat))),
      (ILam ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IData INat), (ISeq ((Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))), (IConst ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), O)))), (ISeq ((Cons ((IData INat), (Cons ((IData
      INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))), (IVar ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (Next ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IData INat), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat))))))))), (ISeq ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IConst ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), O)), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))))), (IVar ((Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))))))))),
      (compile_term g0 (Data t1) e1))), (IRead
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IConst
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), O)))))
  | Inr (g0, t1, t2, e1) -> IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IData INat), (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IData INat))),
      (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat), (IArrow ((IData INat), (IData INat))),
      (ILam ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IData INat), (ISeq ((Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))), (IConst ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (S O))))), (ISeq ((Cons ((IData INat), (Cons ((IData
      INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))), (IVar ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (Next ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat), (IData INat), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IData INat))))))))), (ISeq ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (IWrite ((Cons ((IData INat), (Cons
      ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IConst ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), O)), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (ISucc ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IVar ((Cons ((IData INat), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))))), (IVar ((Cons ((IData INat),
      (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))))), (IData INat), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
       in map g0))), (IData INat))))))))))))))),
      (compile_term g0 (Data t2) e1))), (IRead
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), (IConst
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t0) -> Cons ((compile_ty a), (map t0))
        in map g0), O)))))
  | Case (g0, t1, t2, t0, e0, e1, e2) -> IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IArrow ((IData INat), (compile_ty t0))),
      (compile_ty t0), (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IArrow ((IData INat), (compile_ty t0))), (IArrow
      ((IArrow ((IData INat), (compile_ty t0))), (compile_ty t0))), (IApp
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IData INat), (IArrow ((IArrow ((IData INat),
      (compile_ty t0))), (IArrow ((IArrow ((IData INat), 
      (compile_ty t0))), (compile_ty t0))))), (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IData INat), (IArrow ((IArrow ((IData INat),
      (compile_ty t0))), (IArrow ((IArrow ((IData INat), 
      (compile_ty t0))), (compile_ty t0))))), (ILam ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))), (IArrow ((IData INat), (compile_ty t0))), (IArrow
      ((IArrow ((IData INat), (compile_ty t0))), (compile_ty t0))), (ILam
      ((Cons ((IArrow ((IData INat), (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IArrow ((IData INat), (compile_ty t0))),
      (compile_ty t0), (IIf ((Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (compile_ty t0), (IRead ((Cons ((IArrow ((IData
      INat), (compile_ty t0))), (Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (ISucc ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IVar ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IData INat), (Next ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IData INat), (IArrow ((IData INat),
      (compile_ty t0))), (Next ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))), (IData INat), (IArrow ((IData INat), 
      (compile_ty t0))), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IData INat))))))))))))), (IApp ((Cons ((IArrow ((IData
      INat), (compile_ty t0))), (Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IData INat), (compile_ty t0), (IVar ((Cons ((IArrow
      ((IData INat), (compile_ty t0))), (Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IArrow ((IData INat), (compile_ty t0))), (Next
      ((Cons ((IArrow ((IData INat), (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IArrow ((IData INat), (compile_ty t0))), (IArrow
      ((IData INat), (compile_ty t0))), (First ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))), (IArrow ((IData INat), (compile_ty t0))))))))), (IRead
      ((Cons ((IArrow ((IData INat), (compile_ty t0))), (Cons ((IArrow
      ((IData INat), (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (ISucc ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (ISucc ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IVar ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IData INat), (Next ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IData INat), (IArrow ((IData INat),
      (compile_ty t0))), (Next ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))), (IData INat), (IArrow ((IData INat), 
      (compile_ty t0))), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IData INat))))))))))))))))), (IApp ((Cons ((IArrow
      ((IData INat), (compile_ty t0))), (Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IData INat), (compile_ty t0), (IVar ((Cons ((IArrow
      ((IData INat), (compile_ty t0))), (Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IArrow ((IData INat), (compile_ty t0))), (First
      ((Cons ((IArrow ((IData INat), (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IArrow ((IData INat), (compile_ty t0))))))), (IRead
      ((Cons ((IArrow ((IData INat), (compile_ty t0))), (Cons ((IArrow
      ((IData INat), (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (ISucc ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (ISucc ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IVar ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IArrow ((IData INat), 
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))))), (IData INat), (Next ((Cons ((IArrow ((IData INat),
      (compile_ty t0))), (Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))))), (IData INat), (IArrow ((IData INat),
      (compile_ty t0))), (Next ((Cons ((IData INat),
      (let rec map = function
         | Nil -> Nil
         | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
       in map g0))), (IData INat), (IArrow ((IData INat), 
      (compile_ty t0))), (First
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (IData INat))))))))))))))))))))))))),
      (compile_term g0 (Data (Sum (t1, t2))) e0))), (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (compile_ty (Data t2)), (compile_ty t0),
      (compile_term (Cons ((Data t2), g0)) t0 e2))))), (ILam
      ((let rec map = function
          | Nil -> Nil
          | Cons (a, t3) -> Cons ((compile_ty a), (map t3))
        in map g0), (compile_ty (Data t1)), (compile_ty t0),
      (compile_term (Cons ((Data t1), g0)) t0 e1))))