(data expr
[Var (name : Symbol)]
[abs (name : Symbol) (body : expr)]
[app (fn : expr) (arg : expr)]
[pi (name : Symbol) (e : expr) (body : expr)]
[type (level : Integer)]
[nat]
[zero]
[succ (n : expr)]
[rec expr expr expr expr]
[id expr expr expr]
[refl expr]
[J expr expr expr expr expr expr])