Not really all that exciting, is it?
Anyway. Got a lot more thesis hacking done today. Digging into the algorithmic equality stuff. I think it really is necessary to keep track of relevance labels in contexts, but I don't think I'm going to need to check algorithmic self-equality at the irrelevant application structural equality rule, for instance. Sadly, I may not have enough time to fit unification results into the thesis.
