Use substitutions rather than open (close c x) e

The typing rules in Pulse and Reflection were written when we did not have substitutions as first class entities. As a result, rules often say `open (close c x) e` to mean `subst [NT x e] c` etc. We should migrate to the latter version; one advantage is that the latter is directly amenable to substitution lemmas.

Start by locating the typing rules in Pulse and Reflection that use `open (close c x) e` instead of `subst [NT x e] c`. Migrate those rules to the substitution form and verify that the updated rules are directly usable with substitution lemmas.

Written by the indexing model from the issue text.