moving lookupo around
small refactoring
added bigger typing ex. also still objectify unif
fancy proof tree ex