module Lambda(Node : Set) where open import GeneralLemmas infixl 1 _$_ data Term : Set where ƛ_ : Term → Term _$_ : (t t' : Term) → Term var : ℕ → Term lit : ℕ → Term op : (f : ℕ → ℕ → ℕ)(t t' : Term) → Term if0_then_else_ : (b t f : Term) → Term _at_ : Term → Node → Term