type var = Ix of int

type 'a binder = B of 'a

type term 
  = Var  of var

  | Type

  | T0
  | Ind0 of term binder * term

  | T1
  | T1tr (* Unit eta rule instead of elimination principle *)

  | TNat
  | Zero
  | Suc  of term
  | IndN of term binder * term * term binder binder * term

  | TBool
  | True
  | False
  | IndB of term binder * term * term * term (* ordered true, false *)

  | Pi   of term * term binder
  | Lam  of term binder
  | App  of term * term

  | Sg   of term * term binder
  | Pair of term * term
  | Fst  of term
  | Snd  of term

  | Let  of term * term * term binder (* tr : ty in sc *)