Unification under restriction

[jonsterling]

Now it's time to find out what it means to do unification under a restriction r=r'. The issue is that the naive version results in unleashing solutions that only make sense where r=r'.

I think that what we should do is have the solutions get added to the dev context in terms of that 'partial type' (see #71), and we would only allow them to be unwrapped in case the assumed equation actually holds at the current world.