For example, one with the gathering of the typing relation, and one for the type variable equations, one aspect for unification.
