I certainly can't remove compatibility rules from my reduction since that will preclude CBV essentially, which means I do need them in both
I wrote them in substitution form instead of explicitly for each form for reduction in my rules and surprisingly it works for my proofs
It's just not very algorithmic if you're implementing it
I mean it's pretty much the same structure as the definition of substitution (which... I haven't written out in full either) so it's obvious enough that they're the same
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.