Made a little headway solving some notational issues I was having with unification. I really hope I can knock through this stuff before the end of the summer...