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