type tm =
  | Var of int
  | Pi of tm * (* BINDS *) tm
  | Lam of (* BINDS *) tm
  | App of tm * tm
  | Sg of tm * (* BINDS *) tm
  | Pair of tm * tm
  | Fst of tm
  | Snd of tm
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive : (* BINDS *) tm;
      true_case : tm;
      false_case : tm;
      scrut : tm;
    }