lambda.agda

open import Data.String
open import Data.List
open import Data.List.Any

data Term : Set where
  var : String ->　Term
  lam : String -> Term -> Term
  app : Term -> Term -> Term

sub : Term -> List Term
sub (var sym) = [ var sym ]
sub (lam bind inner) = lam bind inner ∷ sub inner
sub (app left right) = sub left Data.List.++ sub right

sub-refl : (term : Term) -> term ∈ sub term
sub-refl (var sym) = refl