Require Import String.
Open Scope string_scope.
Require Import Lists.ListSet.


Definition variable := string.

Inductive term : Set :=
  | var : variable -> term
  | lam : variable -> term -> term
  | app : term -> term -> term.

Fixpoint freeVariables (t : term) : set variable.

Fixpoint substitute (t : term) (x : variable) (v : term) : term.

Fixpoint alphaEquivalent (t : term) (u : term) : bool.

Definition example1 : term := lam "x" (app (var "x") (var "y")).
Definition example2 : term := lam "f" (lam "f" (app example1 (var "f"))).