> The literature is full of work which erroneously conflates irrelevance in > typechecking with irrelevance in execution. IIUC, the key reason for the difference is that evaluation always proceeds in the empty context, right? Stefan