Goals now keep a history of their resolution process, and Ev terms have a pointer to the goal set that
it generated for type-checking (not for elaboration for now).