General Recursion in Type Theory :
A non-trivial example: Unification
Part 1: data types
type Var = Int
type Fun = Int
data Term = Var Var | Fun Fun [Term]
type Assignment = (Var,Term)
type Substitution = [Assignment]
type Equation = (Term,Term)
type Equations = [Equation]