---
Oh, yeah, it seems I already dealt with this a while ago when I was trying to do proof irrelevance in canonical style. It's a terribly finicky issue with substitution being partial. I can prove [M/x][N/y]P = [[M/x]N/y][M/x]P if both sides are defined, (and y not free in M) but this isn't strong enough; for armed with that only it seems I need to invoke the induction hypotheses twice on the same thing, which potentially gets inductively bigger after the first hit. So I need some lemma that says conclusively that things are defined, not merely use definedness as a premise, and ugh, to really be thorough I will probably have to adapt this bullshit huge technical lemma from the irrelevant-canonical notes.
I shouldn't complain too much, though. I'd be worse off if I hadn't written them in the first place.
---
Eh. Went over the proof over dinner, seems to be fine, and moreover all the particulars seem familiar now that I see them again. It still is such a technical lemma that I fail to have any good intuition for why it should be true, though.
