Bare minimum
Solved constraints generate environments
Equality constraints can bind variables in the environment
Make unification polymorphic over types, half-implement 'and' and 'def'