Inductive term : Type :=
| var (n: nat)
| app (u: term) (v: term)
| lambda (u: term).