got rid of one use of crush, cleaned up helper obligation solving