@lexi.lambda wrt your redex question, I had the following thought: you’re basically trying to define a non-context-free grammar for contexts, which you of course can’t specify just with the BNF style of redex grammars. But certainly you can write a context-sensitive judgment about whether a context is “ok”. Then you can use that either in a side condition in the grammar or a side condition in the reduction-relation definition itself.

@samth Assuming I’m interpreting you correctly, I think I sort of considered that idea, but I wasn’t sure if it made sense or not (or if it would be so slow as to be completely impractical). But if you think it’s not entirely unreasonable, maybe I’ll give it a try.

I think that basically corresponds to what I’d write on paper

Alright, I’ll give it a shot! Thanks!