type t = Data.syn =
  | Var of int
  | Pi of Ident.local * t * (* BINDS *) t
  | Lam of Ident.local * (* BINDS *) t
  | App of t * t
  | Sg of Ident.local * t * (* BINDS *) t
  | Pair of t * t
  | Fst of t
  | Snd of t
  | Type
  | Bool
  | True
  | False
  | BoolElim of {
      motive_var : Ident.local;
      motive : (* BINDS *) t;
      true_case : t;
      false_case : t;
      scrut : t;
    }