Closed oflatt closed 5 months ago
This PR tweaks the substitution rules to preserve InIf contexts. Before, it would throw these away (which is unsound). It also adds back in the context-prop rules to normalize terms, pushing context to leaf nodes.
InIf
This PR tweaks the substitution rules to preserve
InIfcontexts. Before, it would throw these away (which is unsound). It also adds back in the context-prop rules to normalize terms, pushing context to leaf nodes.